swMATH9461MaRDI QIDQ21444FDOQ21444
Author name not available (Why is that?)
Official website: https://abella-prover.org/
Cited In (92)
- Rensets and renaming-based recursion for syntax with bindings
- Proving concurrent constraint programming correct, revisited
- 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
- Automatically generating the dynamic semantics of gradually typed languages
- QML
- 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
- Lolli
- 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 effectiveness of higher-order logic programming in language-oriented programming
- Title not available (Why is that?)
- HYBRID
- Beluga
- LETOS
- Prolog
- Twelf
- MontiCore
- Realizing the dependently typed \(\lambda\)-calculus
- CERES
- Bedwyr
- Minlog
- Tac
- Gmeta
- LNgen
- PoplMark
- Nominal Isabelle
- LeoPARD
- Inductive beluga: programming proofs
- Formalization of a polymorphic subtyping algorithm
- FreshML
- Programming inductive proofs. A new approach based on contextual types
- Reasoning with higher-order abstract syntax and contexts: a comparison
- MetaEdit+
- SugarJ
- LLFp
- CLF
- Delphin
- Elf
- LogAnswer
- SPEC
- Teyjus
- Autosubst
- mini-ML
- CRSX
- Neverlang
- PureScript
- ELPI
- Psi-calculi
- Centaur
- PRIZ
- Logipedia
- 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)
- GHCi
- A two-level logic approach to reasoning about computations
- Implementing type theory in higher order constraint logic programming
- metalib
- lang-n-play
- Harpoon
- The undecidability of proof search when equality is a logical connective
- On the expressivity of minimal generic quantification
- 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
- GMeta: a generic formal metatheory framework for first-order representations
- Reasoning in Abella about structural operational semantics specifications
- A semantics for nabla
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
- On the role of names in reasoning about \(\lambda\)-tree syntax specifications
- There is no best \(\beta \)-normalization strategy for higher-order reasoners
- 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
- Abella: a tutorial
- Constraint handling rules with binders, patterns and generic quantification
- Mechanizing the metatheory of mini-XQuery
This page was built for software: Abella
