Mechanizing proofs with logical relations – Kripke-style (Q4691187): Difference between revisions

@@ Property / cites work @@
+On Irrelevance and Algorithmic Equality in Predicative Type Theory
+Normal rank
@@ Property / cites work @@
+Q4281462
@@ Property / cites work: Q4281462 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Strongly typed term representations in Coq
@@ Property / cites work: Strongly typed term representations in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q5713333
@@ Property / cites work: Q5713333 / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
+Normal rank
@@ Property / cites work @@
+Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+On equivalence and canonical forms in the LF type theory
+Normal rank
@@ Property / cites work @@
+Contextual modal type theory
@@ Property / cites work: Contextual modal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q2871867
@@ Property / cites work: Q2871867 / rank @@
+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 @@
+Q3838063
@@ Property / cites work: Q3838063 / rank @@
+Normal rank
@@ Property / cites work @@
+Logical relations for a logical framework
@@ Property / cites work: Logical relations for a logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Mechanizing the metatheory of LF
@@ Property / cites work: Mechanizing the metatheory of LF / rank @@
+Normal rank