Constructions: A higher order proof system for mechanizing mathematics

Thierry Coquand, Gérard Huet
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]

EUROCAL '85: European Conference on Computer Algebra Linz, Austria, April 1-3 1985 Proceedings Vol. 1: Invited Lectures
Springer
Berlin, Heidelberg
Pages 151-184
1985
Note(s): Coq theorem prover