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

@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ALF
@@ Property / describes a project that uses: ALF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Beluga
@@ Property / describes a project that uses: Beluga / 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-319-21401-6_18
+Normal rank
@@ Property / OpenAlex ID @@
+W1433844459
@@ Property / OpenAlex ID: W1433844459 / rank @@
+Normal rank
@@ 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