A compact kernel for the calculus of inductive constructions (Q1040007): Difference between revisions

@@ Property / describes a project that uses @@
+LEGO
@@ Property / describes a project that uses: LEGO / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2038098277
@@ Property / OpenAlex ID: W2038098277 / rank @@
+Normal rank
@@ Property / cites work @@
+Termination checking with types
@@ Property / cites work: Termination checking with types / rank @@
+Normal rank
@@ Property / cites work @@
+A categorical understanding of environment machines
+Normal rank
@@ Property / cites work @@
+About the Formalization of Some Results by Chebyshev in Number Theory
+Normal rank
@@ Property / cites work @@
+Crafting a Proof Assistant
@@ Property / cites work: Crafting a Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Theoretical Pearls:<i>Representing ‘undefined’ in lambda calculus</i>
+Normal rank
@@ Property / cites work @@
+CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q4484336
@@ Property / cites work: Q4484336 / rank @@
+Normal rank
@@ Property / cites work @@
+Strongly reducing variants of the Krivine abstract machine
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+Q4411846
@@ Property / cites work: Q4411846 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3685171
@@ Property / cites work: Q3685171 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435473
@@ Property / cites work: Q4435473 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692880
@@ Property / cites work: Q4692880 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I
+Normal rank
@@ Property / cites work @@
+Q4364399
@@ Property / cites work: Q4364399 / rank @@
+Normal rank