A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

DOI10.1007/978-3-642-02273-9_3zbMath1246.03025OpenAlexW1690628218MaRDI QIDQ3637183

Andreas Abel, Miguel Pagano, Thierry Coquand

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02273-9_3

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

Reduction Free Normalisation for a proof irrelevant type of propositions ⋮ Unnamed Item

Uses Software

• Coq
• Automath
• Epigram

Cites Work

• Kripke-style models for typed lambda calculus
• Generalized algebraic theories and contextual categories
• An algorithm for type-checking dependent types
• A compiled implementation of strong reduction
• A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Towards a mechanized metatheory of standard ML
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• On the strength of proof-irrelevant type theories
• Subset Coercions in Coq
• A framework for defining logics
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Operational aspects of untyped Normalisation by Evaluation
• Propositions as [Types]
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Extensional equivalence and singleton types
• Advanced Functional Programming
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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