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)

• Rensets and renaming-based recursion for syntax with bindings
• Proving concurrent constraint programming correct, revisited
• A semantics for nabla
• Generic methods for formalising sequent calculi applied to provability logic
• A characterisation of open bisimilarity using an intuitionistic modal logic
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Automatically generating the dynamic semantics of gradually typed languages
• Mechanized metatheory revisited
• Formalized meta-theory of sequent calculi for substructural logics
• Functions-as-constructors higher-order unification: extended pattern unification
• Proof checking and logic programming
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Proof checking and logic programming
• Nominal SOS
• 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
• A case study in programming coinductive proofs: Howe's method
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
• 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
• 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
• Inductive beluga: programming proofs
• Formalization of a polymorphic subtyping algorithm
• Programming inductive proofs. A new approach based on contextual types
• Reasoning with higher-order abstract syntax and contexts: a comparison
• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• A two-level logic approach to reasoning about typed specification languages
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• A two-level logic approach to reasoning about computations
• Implementing type theory in higher order constraint logic programming
• There is no best \(\beta \)-normalization strategy for higher-order reasoners
• The undecidability of proof search when equality is a logical connective
• On the expressivity of minimal generic quantification
• Programming type-safe transformations using higher-order abstract syntax
• 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
• \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
• Harpoon: mechanizing metatheory interactively
• Functions-as-constructors Higher-order Unification
• Abella: a tutorial
• Constraint handling rules with binders, patterns and generic quantification
• GMeta: a generic formal metatheory framework for first-order representations
• Mechanizing the metatheory of mini-XQuery
• Reasoning in Abella about structural operational semantics specifications

This page was built for software: Abella