Beluga
From MaRDI portal
Cited in
(67)- Rensets and renaming-based recursion for syntax with bindings
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- \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
- HYBRID
- Ott
- Twelf
- Abella
- BER MetaOCaml
- Irdis
- Minlog
- Tac
- PLT Redex
- LNgen
- PoplMark
- Nominal Isabelle
- FoCaLiZe
- QuickChick
- RepLib
- VeriML
- TCB
- Idris
- Lincx
- Stardust
- LLFp
- Delphin
- Elf
- MiniAgda
- Forsythe
- Teyjus
- Autosubst
- Celf
- FreshOCaml
- HNT
- Unbound
- Template-Coq
- ELPI
- Psi-calculi
- Focalide
- MiniML
- FreshML
- QML
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- 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
- metalib
- Harpoon
- 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
