A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
From MaRDI portal
Publication:3003322
DOI10.2168/LMCS-7(2:4)2011zbMath1213.68199OpenAlexW2951383623MaRDI QIDQ3003322
Thierry Coquand, Andreas Abel, Miguel Pagano
Publication date: 26 May 2011
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2168/lmcs-7(2:4)2011
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (4)
Efficient extensional binary tries ⋮ Pure type systems with explicit substitutions ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
Uses Software
This page was built for publication: A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
