Abella
From MaRDI portal
Software:21444
No author found.
Related Items (51)
The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ GMeta: A Generic Formal Metatheory Framework for First-Order Representations ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ The undecidability of proof search when equality is a logical connective ⋮ Proof checking and logic programming ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Inductive Beluga: Programming Proofs ⋮ Nominal SOS ⋮ There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners ⋮ Abella: A Tutorial ⋮ A two-level logic approach to reasoning about computations ⋮ A Two-Level Logic Approach to Reasoning about Typed Specification Languages ⋮ Programming Type-Safe Transformations Using Higher-Order Abstract Syntax ⋮ Nominal abstraction ⋮ Constraint handling rules with binders, patterns and generic quantification ⋮ Formalized meta-theory of sequent calculi for linear logics ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Automatically generating the dynamic semantics of gradually typed languages ⋮ A Modular Type Reconstruction Algorithm ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Formalized meta-theory of sequent calculi for substructural logics ⋮ Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Proving concurrent constraint programming correct, revisited ⋮ Proof Checking and Logic Programming ⋮ Generic Methods for Formalising Sequent Calculi Applied to Provability Logic ⋮ Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison ⋮ Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus ⋮ Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) ⋮ Programming Inductive Proofs ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ Formalization of a polymorphic subtyping algorithm ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ On the effectiveness of higher-order logic programming in language-oriented programming ⋮ On the Expressivity of Minimal Generic Quantification ⋮ Reasoning in Abella about Structural Operational Semantics Specifications ⋮ On the Role of Names in Reasoning about λ-tree Syntax Specifications ⋮ Unnamed Item ⋮ Harpoon: mechanizing metatheory interactively ⋮ Mechanizing the Metatheory of mini-XQuery ⋮ Realizing the Dependently Typed Lambda Calculus. ⋮ Implementing type theory in higher order constraint logic programming ⋮ A semantics for nabla ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ Functions-as-constructors Higher-order Unification ⋮ Divergence and unique solution of equations ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ Rensets and renaming-based recursion for syntax with bindings
This page was built for software: Abella
