A Normalizing Intuitionistic Set Theory with Inaccessible Sets

DOI10.2168/LMCS-3(3:6)2007MaRDI QIDQ5426072zbMATH OpenOpenAlexFDO

Authors Wojciech Moczydłowski

Publication date 15 November 2007

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-3(3:6)2007

zbMATH Keywords

axiomatizationCurry-Howard isomorphismimpredicative constructive version of Zermelo-Fraenkel set theory with Replacement and \(\omega \)-many inaccessiblesnormalizationweakly-normalizing typed lambda calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50)

Recommendations

• Computer Science Logic
• Normalization of IZF with Replacement
• Normalization of IZF with Replacement
• scientific article; zbMATH DE number 1420782
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics

Cited in

(5)

• Unifying Sets and Programs via Dependent Types
• Unifying sets and programs via dependent types
• Computer Science Logic
• Normalization of IZF with Replacement
• Normalization of IZF with Replacement

Describes a project that uses

Uses Software

• Coq
• Nuprl
• LEGO

This page was built for publication: A Normalizing Intuitionistic Set Theory with Inaccessible Sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5426072)