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