Mechanizing proofs with logical relations – Kripke-style
From MaRDI portal
Publication:4691187
DOI10.1017/S0960129518000154zbMath1400.68193OpenAlexW2887657530WikidataQ113857441 ScholiaQ113857441MaRDI QIDQ4691187
Publication date: 19 October 2018
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129518000154
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Harpoon: mechanizing metatheory interactively ⋮ A case study in programming coinductive proofs: Howe’s method
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
- Strongly typed term representations in Coq
- On Irrelevance and Algorithmic Equality in Predicative Type Theory
- Mechanizing the metatheory of LF
- Logical relations for a logical framework
- A framework for defining logics
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- On equivalence and canonical forms in the LF type theory
- Contextual modal type theory
- Theorem Proving in Higher Order Logics
- Intensional interpretations of functionals of finite type I
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
This page was built for publication: Mechanizing proofs with logical relations – Kripke-style
