dc.contributor.author Moczydlowski, Wojciech en_US dc.date.accessioned 2007-04-04T20:42:37Z dc.date.available 2007-04-04T20:42:37Z dc.date.issued 2006-10-11 en_US dc.identifier.citation http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2006-2051 en_US dc.identifier.uri https://hdl.handle.net/1813/5748 dc.description.abstract We propose a set theory strong enough to interpret powerful type theories underlying proof assistants such as LEGO and also possibly Coq, which at the same time enables program extraction from constructive proofs. For this purpose, we axiomatize impredicative constructive version of Zermelo-Fraenkel set theory IZF with Replacement and $\omega$-many inaccessibles, which we call IZF_{R\omega}. Our axiomatization of IZF_{R\omega} utilizes set terms, an inductive definition of inaccessible sets and mutually recursive nature of equality and membership relations. It allows us to define a weakly-normalizing typed lambda calculus \lambda Z_\omega corresponding to proofs in IZF_{R\omega} according to the Curry-Howard isomorphism principle. We use realizability to prove the normalization theorem, which provides basis for extracting programs from IZF_{R\omega} proofs. en_US dc.format.extent 532052 bytes dc.format.mimetype application/postscript dc.language.iso en_US en_US dc.publisher Cornell University en_US dc.subject computer science en_US dc.subject technical report en_US dc.title A Normalizing Intuitionistic Set Theory with Inaccessible Sets en_US dc.type technical report en_US
﻿