Beluga
From MaRDI portal
Cited in
(67)- HYBRID
- Ott
- metalib
- Harpoon
- Twelf
- \(\mathrm{HO}\pi\) in Coq
- Harpoon: mechanizing metatheory interactively
- FreshML
- Rensets and renaming-based recursion for syntax with bindings
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Functions-as-constructors higher-order unification: extended pattern unification
- Tac
- Abella
- BER MetaOCaml
- Irdis
- Minlog
- PLT Redex
- PoplMark
- LNgen
- Mechanized metatheory revisited
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Nominal Isabelle
- FoCaLiZe
- QuickChick
- RepLib
- VeriML
- TCB
- A higher-order abstract syntax approach to verified transformations on functional programs
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Programming type-safe transformations using higher-order abstract syntax
- Extensible Datasort Refinements
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Higher-order dynamic pattern unification for dependent types and records
- Programming inductive proofs. A new approach based on contextual types
- Idris
- Stardust
- Lincx
- LLFp
- MiniAgda
- Elf
- Teyjus
- Delphin
- Forsythe
- Unbound
- HNT
- FreshOCaml
- Autosubst
- Celf
- Inductive beluga: programming proofs
- There is no best \(\beta \)-normalization strategy for higher-order reasoners
- Template-Coq
- ELPI
- Psi-calculi
- Focalide
- MiniML
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- A Modular Type Reconstruction Algorithm
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- POPLMark reloaded: mechanizing proofs by logical relations
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Binders unbound
- A case study in programming coinductive proofs: Howe's method
- \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
- Functions-as-constructors Higher-order Unification
- Reasoning with higher-order abstract syntax and contexts: a comparison
- QML
- Mechanizing type environments in weak HOAS
This page was built for software: Beluga
