Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

DOI10.1007/978-3-642-14203-1_2zbMath1291.68366OpenAlexW1536129331MaRDI QIDQ5747747

Joshua Dunfield, Brigitte Pientka

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

Mathematics Subject Classification ID

Related Items (25)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ Inductive Beluga: Programming Proofs ⋮ A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ Finitary type theories with and without contexts ⋮ Towards substructural property-based testing ⋮ Mechanizing type environments in weak HOAS ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Semantical analysis of contextual types ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Extensible Datasort Refinements ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ A logical framework combining model and proof theory ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Programming Inductive Proofs ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Plugging-in proof development environments usingLocksinLF ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Beluga ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• Twelf
• Abella
• Delphin

Cites Work

• Verifying termination and reduction properties about higher-order logic programs
• Case Analysis of Higher-Order Data
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• The Abella Interactive Theorem Prover (System Description)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• Unnamed Item
• Unnamed Item

This page was built for publication: Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)