swMATH1321MaRDI QIDQ14061FDOQ14061
Author name not available (Why is that?)
Official website: http://www.cs.mcgill.ca/~complogic/beluga/
Cited In (66)
- 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
- QML
- 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?)
- HYBRID
- Twelf
- Abella
- BER MetaOCaml
- Irdis
- Minlog
- Tac
- PLT Redex
- LNgen
- PoplMark
- Nominal Isabelle
- FoCaLiZe
- QuickChick
- RepLib
- VeriML
- TCB
- Mechanizing type environments in weak HOAS
- Inductive beluga: programming proofs
- FreshML
- Programming inductive proofs. A new approach based on contextual types
- Reasoning with higher-order abstract syntax and contexts: a comparison
- Idris
- Lincx
- Stardust
- LLFp
- Delphin
- Elf
- MiniAgda
- Forsythe
- Teyjus
- Autosubst
- Celf
- FreshOCaml
- HNT
- Unbound
- Template-Coq
- ELPI
- Psi-calculi
- Focalide
- MiniML
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Binders unbound
- Extensible Datasort Refinements
- POPLMark reloaded: mechanizing proofs by logical relations
- metalib
- Harpoon
- 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
