Research-wise, I am a computer scientist with a tendency to mathematics who ended up in logic. My research can be placed in proof theory, more specifically, I am interested in structural proof theory, logical frameworks, and formal reasoning. If you have no idea what any of this means, and are interested in knowing, read on.
Structural Proof Theory
Structural proof theory is the study of the structure of proofs. In this realm, proofs are like any other mathematical object (like numbers, polynomials, vectors, etc), meaning that they are precisely defined, have a set of properties, and can be operated on. As you may imagine, if we want to perform operations with proofs, they cannot be written as a text argument in English (or any natural language). Therefore, in structural proof theory, statements to be proved are logical formulas and proofs are (most of the time) trees that transform logical formulas. The collection of rules for constructing a proof tree is called a proof system, and different sets of rules (i.e. different proof systems) can represent different logics. Some topics in structural proof theory I am interested in are:
- Coming up with “good” proof systems for different logics
- Formalizing and proving properties of proof systems (see Formal Reasoning below)
- Developing user friendly software for constructing proofs and analyzing proof systems
Logical Frameworks
Logical frameworks are implementations of proof systems (defined above) as tools that can be used to specify and prove properties about systems. Implementing a proof system that is already precisely defined mathematically may seem like an easy task, but it is typically more complicated than one anticipates. There are many hidden assumptions we make on paper that suddenly need to be made explicit, and a series of design choices that will impact the tools efficiency and usability. A really good introduction to the fundamental components of logical framework, and some of the approaches used, is this paper by Frank Pfenning. Examples of different logical frameworks are: Twelf, Isabelle, and Agda. This is far from a comprehensive list, and these systems were chosen for the simple fact that their wikipedia pages include code so that one can easily compare each other. Some topics in logical frameworks I am interested in are:
- The design of a linear logic framework
- Why and how seemingly inoffensive design choices affect usability
Formal Reasoning
Once a logical framework reaches a mature enough state, with a decent specification and proof languages, and a few useful libraries, it is promoted to the rank of proof assistant (also called interactive theorem prover). Formal reasoning is the field that uses proof assistants to specify and proof properties about systems. Here you can think of “systems” in the most general way, e.g., programming languages, robot planning, automata, distributed system, access control rules, cryptocurrencies, smart contracts… etc. If we can faithfully implement the system of interest in the language of the proof assistant, then we can prove properties about it. This is the ultimate way to show that a system behaves as expected. There is a very nice survey about formalized proofs by Talia Ringer et. al. It is long, but reasonably easy to read, quite comprehensive, and it includes a reading guide on section 1.4 in case you want to skip directly to a part of interest. I am not going to list topics in formal reasoning I am interested in, because I am always up for it!
Ultimately, what I really enjoy is organizing reasoning and arguments in sound, elegant, and air-tight formal proofs 😉
You can find a list of publications here and talks here. I like that my projects are accompanied by a software development, some of which can be seen here.