Beluga

swMATH1321MaRDI QIDQ14061FDOQ14061

Author name not available (Why is that?)

Described by source

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

Cited In (27)

• A case study in programming coinductive proofs: Howe’s method
• Rensets and renaming-based recursion for syntax with bindings
• A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• Proof Pearl: Abella Formalization of λ-Calculus Cube Property
• Mechanized metatheory revisited
• Functions-as-constructors higher-order unification: extended pattern unification
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• A Modular Type Reconstruction Algorithm
• Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
• POPLMark reloaded: Mechanizing proofs by logical relations
• LINCX: A Linear Logical Framework with First-Class Contexts
• \(\mathrm{HO}\pi\) in Coq
• Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
• Title not available (Why is that?)
• Higher-Order Dynamic Pattern Unification for Dependent Types and Records
• Mechanizing type environments in weak HOAS
• Binders unbound
• $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
• Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
• Extensible Datasort Refinements
• Programming Inductive Proofs
• Harpoon: mechanizing metatheory interactively
• Inductive Beluga: Programming Proofs
• Functions-as-constructors Higher-order Unification

This page was built for software: Beluga