Details

Autor(en) / Beteiligte

• Miquel, Alexandre

Titel

A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory

Ist Teil von

• Computer Science Logic, 2003, p.441-454

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

2003

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• We propose a method for realising the proofs of Intuitionistic Zermelo-Fraenkel set theory (IZF) by strongly normalising λ-terms. This method relies on the introduction of a Curry-style type theory extended with specific subtyping principles, which is then used as a low-level language to interpret IZF via a representation of sets as pointed graphs inspired by Aczel’s hyperset theory. As a consequence, we refine a classical result of Myhill and Friedman by showing how a strongly normalising λ-term that computes a function of type ℕ→ℕ can be extracted from the proof of its existence in IZF.