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)

• Rensets and renaming-based recursion for syntax with bindings
• \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
• \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 Modular Type Reconstruction Algorithm
• A case study in programming coinductive proofs: Howe's method
• \(\mathrm{HO}\pi\) in Coq
• Title not available (Why is that?)
• Mechanizing type environments in weak HOAS
• Inductive beluga: programming proofs
• Programming inductive proofs. A new approach based on contextual types
• Reasoning with higher-order abstract syntax and contexts: a comparison
• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• Binders unbound
• Extensible Datasort Refinements
• POPLMark reloaded: mechanizing proofs by logical relations
• There is no best \(\beta \)-normalization strategy for higher-order reasoners
• Programming type-safe transformations using higher-order abstract syntax
• A higher-order abstract syntax approach to verified transformations on functional programs
• Harpoon: mechanizing metatheory interactively
• Functions-as-constructors Higher-order Unification
• \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

This page was built for software: Beluga