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
Program
Social Program
Registration
Location and Venue
Accommodation
Committees
Contact
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