# Talk by Emilia Maietti (LTCS)

**Venue:**

Room A097, ExWi, Sidlerstrasse 5, 3012 Bern

**Speaker:**

Prof. Dr. Maria Emilia Maietti (UniversitÃ di Padova )

**Title:**

Properties discriminating the Minimalist Foundation from Martin-Loef's type theory

**Abstract:**

We compare the Minimalist Foundation, ideated in [MS05] and completed to a two-level system in [M09],

with Martin-Loef's type theory in [M84],[NPS90], by outlining the common and different aspects.

In particular we will focus on some properties discriminating the Minimalist Foundation from Martin-Loef's type theory.

These properties will include

- compatibility with most relevant constructive and classical foundations;
- consistency with formal Church thesis;
- conservativity over first order intuitionistic logic.

As a byproduct of our comparison we motivate the use of Martin-Loef's intensional type theory as a realizability theory where to extract programs from proofs in the Minimalist Foundation.

[MS05] Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides,pp. 91-114. Oxford University Press (2005)

[M09] Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic 160(3), 319{354 (2009)

[M84] Martin-Loef, P.: Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Naples (1984)

[NPS90] Nordstrom, B., Petersson, K., Smith, J.: Programming in Martin Lof's Type Theory. Clarendon Press, Oxford (1990)

- Log in to post comments