Pages that link to "Item:Q438569"
From MaRDI portal
The following pages link to Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569):
Displaying 23 items.
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- Canonical HybridLF: extending Hybrid with dependent types (Q1744412) (← links)
- Cut elimination for a logic with induction and co-induction (Q1948276) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of metatheory of the Quipper quantum programming language in a linear logic (Q2331074) (← links)
- Formal meta-level analysis framework for quantum programming languages (Q2333324) (← links)
- Mechanizing focused linear logic in Coq (Q2333326) (← links)
- Term-generic logic (Q2339466) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- A hybrid encoding of Howe's method for establishing congruence of bisimilarity (Q2844810) (← links)
- Two-level hybrid: a system for reasoning using higher-order abstract syntax (Q2871875) (← links)
- Programs Using Syntax with First-Class Binders (Q2988654) (← links)
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions (Q4691183) (← links)
- Mechanizing proofs with logical relations – Kripke-style (Q4691187) (← links)
- A focused linear logical framework and its application to metatheory of object logics (Q5022931) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- Relating system F and \(\lambda 2\): a case study in Coq, Abella and Beluga (Q5111317) (← links)
- A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
- Towards substructural property-based testing (Q6102253) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
