Types for Proofs and Programs

DOI10.1007/11617990MaRDI QIDQ5898169zbMATH OpenOpenAlexFDO

Authors Robin Adams

Publication date 13 November 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11617990

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65)

Recommendations

• Engineering formal metatheory
• A formalized general theory of syntax with bindings: extended version
• Strongly typed term representations in Coq
• A formalized general theory of syntax with bindings
• GMeta: a generic formal metatheory framework for first-order representations

Cited in

(8)

• A formalized general theory of syntax with bindings: extended version
• Strongly typed term representations in Coq
• Some Domain Theory and Denotational Semantics in Coq
• Engineering formal metatheory
• Formalizing the meta-theory of first-order predicate logic
• POPLMark reloaded: mechanizing proofs by logical relations
• Tower induction and up-to techniques for CCS with fixed points
• scientific article; zbMATH DE number 5033853 (Why is no real title available?)

Describes a project that uses

Uses Software

• Automath
• Coq

This page was built for publication: Types for Proofs and Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5898169)