\texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108): Difference between revisions

@@ Property / cites work @@
+Towards certified meta-programming with typed Template-Coq
+Normal rank
@@ Property / cites work @@
+A trustworthy proof checker
@@ Property / cites work: A trustworthy proof checker / rank @@
+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 @@
+Idris, a general-purpose dependently typed programming language: Design and implementation
+Normal rank
@@ Property / cites work @@
+Q4281470
@@ Property / cites work: Q4281470 / rank @@
+Normal rank
@@ Property / cites work @@
+ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
+Normal rank
@@ Property / cites work @@
+Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
+Normal rank
@@ Property / cites work @@
+Operational semantics of resolution and productivity in Horn clause logic
+Normal rank
@@ Property / cites work @@
+Some logical and syntactical observations concerning  the first-order dependent type system λP
+Normal rank
@@ Property / cites work @@
+Implementing type theory in higher order constraint logic programming
+Normal rank
@@ Property / cites work @@
+On equivalence and canonical forms in the LF type theory
+Normal rank
@@ Property / cites work @@
+An insider's look at LF type reconstruction: everything you (n)ever wanted to know
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+Ott
@@ Property / cites work: Ott / rank @@
+Normal rank
@@ Property / cites work @@
+The \textsc{MetaCoq} project
@@ Property / cites work: The \textsc{MetaCoq} project / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing the metatheory of LF
@@ Property / cites work: Mechanizing the metatheory of LF / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal unification
@@ Property / cites work: Nominal unification / rank @@
+Normal rank