Pages that link to "Item:Q3541698"
From MaRDI portal
The following pages link to The Abella Interactive Theorem Prover (System Description) (Q3541698):
Displaying 22 items.
- Abella (Q21444) (← links)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Proving concurrent constraint programming correct, revisited (Q530860) (← links)
- Nominal abstraction (Q617715) (← links)
- TWAM: a certifying abstract machine for logic programs (Q1629962) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of metatheory of the Quipper quantum programming language in a linear logic (Q2331074) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- On the Expressivity of Minimal Generic Quantification (Q2804937) (← links)
- Reasoning in Abella about Structural Operational Semantics Specifications (Q2804943) (← links)
- On the Role of Names in Reasoning about λ-tree Syntax Specifications (Q2804945) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- The Abella Interactive Theorem Prover (System Description) (Q3541698) (← links)
- Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
- A semantics for nabla (Q5236555) (← links)
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus (Q5747746) (← links)
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) (Q5747747) (← links)
