The following pages link to Beluga (Q14061):
Displaying 27 items.
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of metatheory of the Quipper quantum programming language in a linear logic (Q2331074) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax (Q2938052) (← links)
- Extensible Datasort Refinements (Q2988653) (← links)
- LINCX: A Linear Logical Framework with First-Class Contexts (Q2988658) (← links)
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (Q3007654) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners (Q3460064) (← links)
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (Q4559809) (← links)
- A Modular Type Reconstruction Algorithm (Q4617969) (← links)
- Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- Relating system F and \(\lambda 2\): a case study in Coq, Abella and Beluga (Q5111317) (← links)
- Binders unbound (Q5176984) (← links)
- A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
- $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (Q5278085) (← links)
- Functions-as-constructors Higher-order Unification (Q5369491) (← links)
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison (Q5747652) (← links)
