Type Theory and Formal Proof

DOI10.1017/CBO9781139567725zbMath1317.03001MaRDI QIDQ2925448

Herman Geuvers, Rob Nederpelt

Publication date: 22 October 2014

Mathematics Subject Classification ID

03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations

03F07: Structure of proofs

03F03: Proof theory in general (including proof-theoretic semantics)

Uses Software

• Coq
• Mizar
• HOL