The following pages link to Abella (Q21444):
Displaying 50 items.
- 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)
- Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings (Q951681) (← links)
- Formalized meta-theory of sequent calculi for substructural logics (Q1744443) (← links)
- Formalization of a polymorphic subtyping algorithm (Q1791209) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- On the effectiveness of higher-order logic programming in language-oriented programming (Q2039939) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- The undecidability of proof search when equality is a logical connective (Q2134939) (← 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)
- Formalized meta-theory of sequent calculi for linear logics (Q2424887) (← links)
- Proof checking and logic programming (Q2628296) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← 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 \(\lambda\)-tree syntax specifications (Q2804945) (← links)
- Realizing the dependently typed \(\lambda\)-calculus (Q2883111) (← links)
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations (Q2892744) (← links)
- Abella: A Tutorial (Q2914731) (← links)
- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax (Q2938052) (← links)
- A Two-Level Logic Approach to Reasoning about Typed Specification Languages (Q2978545) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- Nominal SOS (Q3178277) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners (Q3460064) (← links)
- Constraint handling rules with binders, patterns and generic quantification (Q4592722) (← links)
- A Modular Type Reconstruction Algorithm (Q4617969) (← links)
- Proof-relevant π-calculus: a constructive account of concurrency and causality (Q4691184) (← links)
- Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
- Generic Methods for Formalising Sequent Calculi Applied to Provability Logic (Q4933310) (← links)
- Relating system F and \(\lambda 2\): a case study in Coq, Abella and Beluga (Q5111317) (← links)
- Divergence and unique solution of equations (Q5111619) (← links)
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem (Q5204803) (← links)
- Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
- A semantics for nabla (Q5236555) (← links)
- A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
- Functions-as-constructors Higher-order Unification (Q5369491) (← links)
- Automatically generating the dynamic semantics of gradually typed languages (Q5370913) (← links)
- Proof Checking and Logic Programming (Q5743582) (← links)
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison (Q5747652) (← links)
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus (Q5747746) (← links)
