
We propose a method for realising the proofs of Intuitionistic ZermeloFraenkel set theory (IZF) by strongly normalising lambdaterms. This method relies on the introduction of a Currystyle type theory extended with specific subtyping principles, which is then used as a lowlevel 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 lambdaterm that computes a function of type N>N can be extracted from the proof of its existence in IZF.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 