Strongly typed term representations in Coq
From MaRDI portal
Publication:2392480
DOI10.1007/S10817-011-9219-0zbMATH Open1269.68041DBLPjournals/jar/BentonHKM12OpenAlexW1997354605WikidataQ56851585 ScholiaQ56851585MaRDI QIDQ2392480FDOQ2392480
Authors: Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride 
Publication date: 1 August 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9219-0
Recommendations
Cites Work
- Title not available (Why is that?)
- A framework for defining logics
- Title not available (Why is that?)
- Parametric higher-order abstract syntax for mechanized semantics
- Biorthogonality, step-indexing and compiler correctness
- Program-ing finger trees in C <scp>oq</scp>
- The view from the left
- de Bruijn notation as a nested datatype
- Title not available (Why is that?)
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Guarded recursive datatype constructors
- Some Domain Theory and Denotational Semantics in Coq
- Nested abstract syntax in Coq
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- Types for Proofs and Programs
Cited In (10)
- Title not available (Why is that?)
- A case study in programming coinductive proofs: Howe’s method
- Semantic analysis of normalisation by evaluation for typed lambda calculus
- Programs Using Syntax with First-Class Binders
- Types for Proofs and Programs
- POPLMark reloaded: Mechanizing proofs by logical relations
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Mechanizing proofs with logical relations – Kripke-style
- A linear algebra approach to linear metatheory
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
Uses Software
This page was built for publication: Strongly typed term representations in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2392480)
