A minimalist two-level foundation for constructive mathematics

Citations of this article
Mendeley users who have this article in their library.


We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin. One level is given by an intensional type theory, called Minimal type theory. This theory extends a previous version with collections. The other level is given by an extensional set theory that is interpreted in the first one by means of a quotient model. This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the "proofs-as-programs" paradigm and acts as a programming language. © 2009 Elsevier B.V. All rights reserved.




Maietti, M. E. (2009). A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3), 319–354. https://doi.org/10.1016/j.apal.2009.01.006

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free