swMATH421MaRDI QIDQ13181FDOQ13181
Author name not available (Why is that?)
Official website: http://hybrid.di.unimi.it/
Cited In (43)
- 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
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Formal meta-level analysis framework for quantum programming languages
- Mechanized metatheory revisited
- Canonical HybridLF: extending Hybrid with dependent types
- 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
- Lolli
- A case study in programming coinductive proofs: Howe's method
- Alcove
- Title not available (Why is that?)
- Beluga
- Twelf
- Mechanizing focused linear logic in Coq
- Abella
- Bedwyr
- Tac
- Quipper
- PLT Redex
- Gmeta
- LNgen
- Quati
- PoplMark
- Nominal Isabelle
- Lincx
- LLFp
- Delphin
- Autosubst
- Celf
- ELPI
- Psi-calculi
- YALLA
- 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
- Programs using syntax with first-class binders
This page was built for software: HYBRID
