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

DOI10.1007/978-3-642-02273-9_3MaRDI QIDQ3637183zbMATH OpenOpenAlexFDO

Authors Andreas Abel, Thierry Coquand, Miguel Pagano

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)

Recommendations

• A modular type-checking algorithm for type theory with singleton types and proof irrelevance
• Extensional equivalence and singleton types
• scientific article; zbMATH DE number 65534
• An extensible equality checking algorithm for dependent type theories
• A partial type checking algorithm for Type:Type

Cites work

• A compiled implementation of strong reduction
• A framework for defining logics
• A general formulation of simultaneous inductive-recursive definitions in type theory
• A modular type-checking algorithm for type theory with singleton types and proof irrelevance
• Advanced Functional Programming
• An algorithm for type-checking dependent types
• Extensional equivalence and singleton types
• Generalized algebraic theories and contextual categories
• scientific article; zbMATH DE number 1617290 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 2079014 (Why is no real title available?)
• scientific article; zbMATH DE number 2182489 (Why is no real title available?)
• Kripke-style models for typed lambda calculus
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• On the strength of proof-irrelevant type theories
• Operational aspects of untyped Normalisation by Evaluation
• Propositions as [Types]
• Subset Coercions in Coq
• Towards a mechanized metatheory of Standard ML
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

Cited in

(12)

• Modularity of proof-nets. Generating the type of a module.
• On irrelevance and algorithmic equality in predicative type theory
• A modular type-checking algorithm for type theory with singleton types and proof irrelevance
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• scientific article; zbMATH DE number 1746455 (Why is no real title available?)
• An algorithm for checking incomplete proof objects in type theory with localization and unification
• A cubical language for Bishop sets
• A partial type checking algorithm for Type:Type
• Extensional equivalence and singleton types
• Sound and complete elimination of singleton kinds
• Reduction Free Normalisation for a proof irrelevant type of propositions
• Implementing a type theory with observational equality, using normalisation by evaluation

Describes a project that uses

Uses Software

• Epigram
• Coq
• Automath

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3637183)