Inductive Beluga: Programming Proofs (Q3454100): Difference between revisions

@@ Property / cites work @@
+Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
+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 @@
+Programming with binders and indexed data-types
@@ Property / cites work: Programming with binders and indexed data-types / rank @@
+Normal rank
@@ Property / cites work @@
+Case Analysis of Higher-Order Data
@@ Property / cites work: Case Analysis of Higher-Order Data / rank @@
+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 @@
+The Abella Interactive Theorem Prover (System Description)
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+The Alf proof editor and its proof engine
@@ Property / cites work: The Alf proof editor and its proof engine / rank @@
+Normal rank
@@ Property / cites work @@
+Contextual modal type theory
@@ Property / cites work: Contextual modal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
+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 @@
+Q5277845
@@ Property / cites work: Q5277845 / rank @@
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank