Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
From MaRDI portal
Publication:5747747
Recommendations
Cites work
- scientific article; zbMATH DE number 2090533 (Why is no real title available?)
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A framework for defining logics
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Case analysis of higher-order data
- The Abella Interactive Theorem Prover (System Description)
- Two-level hybrid: a system for reasoning using higher-order abstract syntax
- Verifying termination and reduction properties about higher-order logic programs
Cited in
(31)- A logical framework combining model and proof theory
- Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Contextual modal type theory with polymorphic contexts
- Mechanized metatheory revisited
- Functions-as-constructors higher-order unification: extended pattern unification
- Higher-order dynamic pattern unification for dependent types and records
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- A case study in programming coinductive proofs: Howe's method
- \(\mathrm{HO}\pi\) in Coq
- TinkerType: a language for playing with formal systems
- Beluga
- Mechanizing type environments in weak HOAS
- Inductive beluga: programming proofs
- Programming inductive proofs. A new approach based on contextual types
- Mtac: a monad for typed tactic programming in Coq
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Finitary type theories with and without contexts
- Extensible Datasort Refinements
- POPLMark reloaded: mechanizing proofs by logical relations
- Towards substructural property-based testing
- Mechanizing proofs with logical relations -- Kripke-style
- A higher-order abstract syntax approach to verified transformations on functional programs
- Harpoon: mechanizing metatheory interactively
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
- Semantical analysis of contextual types
- Abella: a system for reasoning about relational specifications
- Abella: a tutorial
This page was built for publication: Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747747)
