On the strength of proof-irrelevant type theories
From MaRDI portal
Publication:3535620
DOI10.2168/LMCS-4(3:13)2008zbMath1151.03317OpenAlexW3101932690MaRDI QIDQ3535620
Publication date: 13 November 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(3:13)2008
theorem provingtype theoryaxiom of choiceprototype verification systemproof-irrelevanceset-theoretic semanticsconversion ruleadditional extentionality
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
An intuitionistic set-theoretical model of fully dependent CC ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
Uses Software
This page was built for publication: On the strength of proof-irrelevant type theories
