Show simple item record

dc.contributor.authorMoczydlowski, Wojciechen_US
dc.description.abstractWe 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.extent532052 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleA Normalizing Intuitionistic Set Theory with Inaccessible Setsen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record