A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (Q3637183): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-02273-9_3
+Normal rank
@@ Property / OpenAlex ID @@
+W1690628218
@@ Property / OpenAlex ID: W1690628218 / rank @@
+Normal rank
@@ Property / cites work @@
+Normalization by Evaluation for Martin-Löf Type Theory with One Universe
+Normal rank
@@ Property / cites work @@
+On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
+Normal rank
@@ Property / cites work @@
+Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
+Normal rank
@@ Property / cites work @@
+A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
+Normal rank
@@ Property / cites work @@
+Operational aspects of untyped Normalisation by Evaluation
+Normal rank
@@ Property / cites work @@
+Q4474826
@@ Property / cites work: Q4474826 / rank @@
+Normal rank
@@ Property / cites work @@
+Propositions as [Types]
@@ Property / cites work: Propositions as [Types] / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized algebraic theories and contextual categories
+Normal rank
@@ Property / cites work @@
+An algorithm for type-checking dependent types
@@ Property / cites work: An algorithm for type-checking dependent types / rank @@
+Normal rank
@@ Property / cites work @@
+Q4681364
@@ Property / cites work: Q4681364 / rank @@
+Normal rank
@@ Property / cites work @@
+A general formulation of simultaneous inductive-recursive definitions in type theory
+Normal rank
@@ Property / cites work @@
+A compiled implementation of strong reduction
@@ Property / cites work: A compiled implementation of strong reduction / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a mechanized metatheory of standard ML
@@ Property / cites work: Towards a mechanized metatheory of standard ML / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Advanced Functional Programming
@@ Property / cites work: Advanced Functional Programming / rank @@
+Normal rank
@@ Property / cites work @@
+Kripke-style models for typed lambda calculus
@@ Property / cites work: Kripke-style models for typed lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2722014
@@ Property / cites work: Q2722014 / rank @@
+Normal rank
@@ Property / cites work @@
+Subset Coercions in Coq
@@ Property / cites work: Subset Coercions in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Extensional equivalence and singleton types
@@ Property / cites work: Extensional equivalence and singleton types / rank @@
+Normal rank
@@ Property / cites work @@
+On the strength of proof-irrelevant type theories
@@ Property / cites work: On the strength of proof-irrelevant type theories / rank @@
+Normal rank