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
Springer
Berlin, Heidelberg
Pages 151-184
1985
Note(s): Coq theorem prover