Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
From MaRDI portal
Publication:5747747
DOI10.1007/978-3-642-14203-1_2zbMATH Open1291.68366OpenAlexW1536129331MaRDI QIDQ5747747FDOQ5747747
Authors: Brigitte Pientka, Joshua Dunfield 
Publication date: 14 September 2010
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_2
Recommendations
Cites Work
- The Abella Interactive Theorem Prover (System Description)
- A framework for defining logics
- Case analysis of higher-order data
- Two-level hybrid: a system for reasoning using higher-order abstract syntax
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Verifying termination and reduction properties about higher-order logic programs
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Title not available (Why is that?)
Cited In (30)
- 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
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Contextual modal type theory with polymorphic contexts
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- 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
- Mtac: a monad for typed tactic programming in Coq
- Inductive beluga: programming proofs
- Programming inductive proofs. A new approach based on contextual types
- 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
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
- Abella: a system for reasoning about relational specifications
- Semantical analysis of contextual types
- Abella: a tutorial
Uses Software
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)
