Cited in
(44)- Programs using syntax with first-class binders
- Alcove
- Rensets and renaming-based recursion for syntax with bindings
- A linear logic framework for multimodal logics
- A focused linear logical framework and its application to metatheory of object logics
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Formal meta-level analysis framework for quantum programming languages
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Canonical HybridLF: extending Hybrid with dependent types
- Mechanized metatheory revisited
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A formalized general theory of syntax with bindings: extended version
- A case study in programming coinductive proofs: Howe's method
- Ott
- Beluga
- Twelf
- Abella
- Bedwyr
- Tac
- Quipper
- PLT Redex
- Gmeta
- LNgen
- Quati
- PoplMark
- Nominal Isabelle
- Lincx
- LLFp
- Delphin
- Autosubst
- Celf
- ELPI
- Psi-calculi
- YALLA
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Mechanizing focused linear logic in Coq
- Lolli
- Cut elimination for a logic with induction and co-induction
- Sequoia
- A two-level logic approach to reasoning about computations
- POPLMark reloaded: mechanizing proofs by logical relations
- Mechanizing proofs with logical relations -- Kripke-style
- Term-generic logic
This page was built for software: HYBRID
