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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Miquel, A. (2003). A strongly normalising Curry-Howard correspondence for IZF set theory. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2803, 441–454. https://doi.org/10.1007/978-3-540-45220-1_35
Mendeley helps you to discover research relevant for your work.