Research

I am mostly interested in the foundations of constructive mathematics with a particular focus on intuitionism and type theory. Other interests of mine include the history and philosophy of logic in general. In fact, I began my academic career as a Frege scholar working on the Caesar problem and turned to the study of type theory motivated by the theory of value ranges in Grundgesetze. Some of my recent projects still engage with Frege.

One recurrent idea in my work is that the philosophy of mathematics has a lot to gain if type theory is taken seriously as a foundational alternative. Simply put, a type theory is a family of formal systems based on Russell’s idea of annotating objects with types and restricting operations to objects of certain types. The particular flavor of type theory I am interested in was developed by Per Martin-Löf to serve as a full-scale formalization of constructive mathematics, building on the work of earlier authors such as Frege, Russell, Brouwer, Church, Curry, Kreisel, Howard, Scott, and de Bruijn. It corresponds to an enriched form of higher-order constructive logic, where constructions that realize a true proposition are represented by elements of a type.

My view of type theory builds on the intuitionistic view maintained by L. E. J. Brouwer that mathematics is a human mental activity. However, Brouwer originally maintained an account of human mathematical cognition that goes beyond calculability, admitting constructions not only by means of effective rules but also by free choices of mathematical objects that may not be determined effectively. Here I follow Errett Bishop in identifying constructions with informal effective methods or "person programs" to use his own expression. Brouwer and Bishop both emphasized that mathematics rests on human understanding. Borrowing elements from Kant's transcendental project and building on ideas by Robert Constable, I began developing a new foundation of type theory in my book "Philosophical Type Theory" to capture the essence of Brouwer's and Bishop's views as I understand them. This approach represents an alternative to the philosophical foundations of type theory proposed by Martin-Löf in the last four decades.

I am also enthusiastic about the applications of type theory in the formalization of mathematics using iterative theorem provers. In the past, I formalized some completeness proofs for modal and intuitionistic propositional logic using Lean 3 and 4 and contributed some formalized mathematics to Cubical Adga. Lately, I have turned my efforts to the development of the experimental Pearl proof assistant based on the computational type theory developed in my recent book. It is based on a decubicalization of an OCaml implementation that I began writing in 2019 while working at CMU.