Abella

swMATH9461MaRDI QIDQ21444FDOQ21444

Author name not available (Why is that?)

Described by source

• The Abella Interactive Theorem Prover (System Description)
• Abella: A System for Reasoning about Relational Specifications

Cited In (51)

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

This page was built for software: Abella