A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

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

zbMATH Keywords

type theorytype-checkingproof irrelevancesingleton typesnormalisation-by-evaluation

Mathematics Subject Classification ID

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

• Coq
• Automath
• Epigram

This page was built for publication: A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance