Talk by Emilia Maietti (LTCS)

Short Title: 
Talk by Emilia Maietti
Event Date(s): 
Thursday, 12. April 2018 - 10:15 to 11:30

Room A097, ExWi, Sidlerstrasse 5, 3012 Bern

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

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

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)