Strongly typed term representations in Coq

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

zbMATH Keywords

de Bruijn indices\texttt{Coq} proof assistanttyped object languages

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Initial semantics for higher-order typed syntax in \textsf{Coq}
• scientific article; zbMATH DE number 2185657
• Types for Proofs and Programs
• Engineering formal metatheory
• Mechanizing type environments in weak HOAS

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 2085175 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
• A framework for defining logics
• Biorthogonality, step-indexing and compiler correctness
• Guarded recursive datatype constructors
• Nested abstract syntax in Coq
• Parametric higher-order abstract syntax for mechanized semantics
• Program-ing finger trees in Coq
• Some Domain Theory and Denotational Semantics in Coq
• The view from the left
• Types for Proofs and Programs
• de Bruijn notation as a nested datatype

Cited in

(13)

• scientific article; zbMATH DE number 7447767 (Why is no real title available?)
• Engineering formal metatheory
• A linear algebra approach to linear metatheory
• Initial semantics for higher-order typed syntax in \textsf{Coq}
• POPLMark reloaded: mechanizing proofs by logical relations
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• A case study in programming coinductive proofs: Howe's method
• Semantic analysis of normalisation by evaluation for typed lambda calculus
• Mechanizing type environments in weak HOAS
• Programs using syntax with first-class binders
• Deep Generation of Coq Lemma Names Using Elaborated Terms
• Mechanizing proofs with logical relations -- Kripke-style
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• Coq
• Heq

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)