Types for Proofs and Programs

DOI10.1007/b98246zbMath1100.03509OpenAlexW4298423642MaRDI QIDQ5712303

Pierre Corbineau

Publication date: 23 December 2005

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

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (3)

Practical Proof Search for Coq by Type Inhabitation ⋮ Hammer for Coq: automation for dependent type theory ⋮ A Declarative Language for the Coq Proof Assistant

Uses Software

• Coq

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