Beluga
From MaRDI portal
Software:14061
No author found.
Related Items (27)
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 ⋮ There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ Programming Type-Safe Transformations Using Higher-Order Abstract Syntax ⋮ Mechanizing type environments in weak HOAS ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ A Modular Type Reconstruction Algorithm ⋮ Extensible Datasort Refinements ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads ⋮ Binders unbound ⋮ Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison ⋮ Programming Inductive Proofs ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Unnamed Item ⋮ Harpoon: mechanizing metatheory interactively ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ Functions-as-constructors Higher-order Unification ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory
This page was built for software: Beluga