A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
From MaRDI portal
Publication:3637183
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
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
This page was built for publication: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
