Abella
From MaRDI portal
Cited in
(94)- HYBRID
- Ott
- metalib
- lang-n-play
- Harpoon
- Beluga
- lolliCoP
- LETOS
- Formalized meta-theory of sequent calculi for substructural logics
- Formalization of a polymorphic subtyping algorithm
- Prolog
- Twelf
- MontiCore
- A formalized general theory of syntax with bindings: extended version
- \(\mathrm{HO}\pi\) in Coq
- On the effectiveness of higher-order logic programming in language-oriented programming
- Harpoon: mechanizing metatheory interactively
- FreshML
- Rensets and renaming-based recursion for syntax with bindings
- Functions-as-constructors higher-order unification: extended pattern unification
- The undecidability of proof search when equality is a logical connective
- CERES
- Tac
- Bedwyr
- Minlog
- PoplMark
- Gmeta
- LNgen
- Mechanized metatheory revisited
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- A two-level logic approach to reasoning about computations
- Nominal Isabelle
- Formalized meta-theory of sequent calculi for linear logics
- LeoPARD
- Proof checking and logic programming
- A higher-order abstract syntax approach to verified transformations on functional programs
- 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
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Realizing the dependently typed -calculus
- GMeta: a generic formal metatheory framework for first-order representations
- Abella: a tutorial
- Programming type-safe transformations using higher-order abstract syntax
- A two-level logic approach to reasoning about typed specification languages
- Programming inductive proofs. A new approach based on contextual types
- MetaEdit+
- SugarJ
- Mechanizing the metatheory of mini-XQuery
- Nominal SOS
- SPEC
- LLFp
- Elf
- Teyjus
- Delphin
- LogAnswer
- CLF
- Autosubst
- mini-ML
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- Inductive beluga: programming proofs
- There is no best \(\beta \)-normalization strategy for higher-order reasoners
- CRSX
- Neverlang
- PureScript
- ELPI
- Psi-calculi
- Centaur
- PRIZ
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Logipedia
- Constraint handling rules with binders, patterns and generic quantification
- A Modular Type Reconstruction Algorithm
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Generic methods for formalising sequent calculi applied to provability logic
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- A characterisation of open bisimilarity using an intuitionistic modal logic
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Implementing type theory in higher order constraint logic programming
- A semantics for nabla
- A case study in programming coinductive proofs: Howe's method
- Proving concurrent constraint programming correct, revisited
- Functions-as-constructors Higher-order Unification
- Automatically generating the dynamic semantics of gradually typed languages
- GHCi
- Proof checking and logic programming
- 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)
- QML
- Lolli
- Nominal abstraction
- Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
This page was built for software: Abella
