scientific article; zbMATH DE number 7359415
From MaRDI portal
Publication:4993349
DOI10.4230/LIPIcs.FSCD.2018.19zbMath1462.68021arXiv1805.00401MaRDI QIDQ4993349
Brigitte Pientka, Rohan Jacob-Rao, David Thibodeau
Publication date: 15 June 2021
Full work available at URL: https://arxiv.org/abs/1805.00401
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (3)
POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Harpoon: mechanizing metatheory interactively ⋮ A case study in programming coinductive proofs: Howe’s method
Cites Work
- Unnamed Item
- Theorem proving modulo
- Cut elimination for a logic with induction and co-induction
- Stratification in Logics of Definitions
- Programming with binders and indexed data-types
- Guarded recursive datatype constructors
- Indexed codata types
- Combining Deduction Modulo and Logics of Fixed-Point Definitions
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Proof normalization modulo
- Contextual modal type theory
- Computer Science Logic
- Intensional interpretations of functionals of finite type I
- Types for Proofs and Programs
- Reasoning with higher-order abstract syntax in a logical framework
This page was built for publication:
