Computer Science Logic and 8th Kurt Gödel Colloquium
Alexandre Miquel: A Strongly Normalising Curry-Howard correspondence for IZF Set Theory
Welcome and News
Host Institutions
Calls and Deadlines
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
We propose a method for realising the proofs of Intuitionistic Zermelo-Fraenkel set theory (IZF) by strongly normalising lambda-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 lambda-term that computes a function of type N->N can be extracted from the proof of its existence in IZF.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04 Valid HTML 4.01! Valid CSS! Debian