Normalization of IZF with Replacement

DOI10.2168/LMCS-4(2:1)2008zbMath1143.03027OpenAlexW2143619447MaRDI QIDQ5900206

Wojciech Moczydłowski

Publication date: 7 August 2008

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

Full work available at URL: https://doi.org/10.2168/lmcs-4(2:1)2008

zbMATH Keywords

normalizationrealizabilityCurry-Howard isomorphismtyped lambda calculusintuitionistic set theoryinner extensional model

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Nonclassical and second-order set theories (03E70) Combinatory logic and lambda calculus (03B40)