Research

I am particularly interested in themes revolving around mathematical constructivism, with emphasis on connections between intuitionism 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 peculiar conception of construction that goes beyond calculability, admitting constructions not only by means of effective rules but also 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 Erret 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.

Another recurrent idea in my work is that philosophy of mathematics has a lot to gain if type theory is taken seriously as a foundation for mathematics. 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.