Research
I am interested in the philosophical foundations of constructive mathematics, with a particular focus on topics related to intuition and type theory.
My work builds on the intuitionistic tradition of L. E. J. Brouwer and Arend Heyting, according to which mathematical objects are mental constructions given in temporal intuition and the truth of a proposition consists in one's possession of a construction satisfying some properties. However, Brouwer originally proposed his account of intuition against the background of a unique conception of construction 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.
The conception of construction I am rather interested in is the one underlying the more influential brand of constructivism of Errett Bishop, according to which constructions are informal effective methods or, to use his own expression, "person programs". Lately, I have been trying to rearticulate the effective elements of Brouwer's account of intuition and recast them into a novel account of intuition that explains how we gain epistemic access to constructions in Bishop's sense. In contrast to Brouwer's original views, the idea is that this novel account of intuition will exclude non-lawlike constructions as objects of intuition.
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. Now, according to the basic intuitionistic tenet that constructions are objects given to us in intuition, is it possible to understand the elements of a type as objects of intuition?
I am also enthusiastic about the applications of type theory in the formalization of mathematics using proof assistants or iterative theorem provers.