1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
@book{coqart,
title = "Interactive Theorem Proving and Program Development.
Coq'Art: The Calculus of Inductive Constructions",
author = {Yves Bertot and Pierre Castéran},
publisher = "Springer Verlag",
series = "Texts in Theoretical Computer Science. An EATCS series",
year = 2004
}
@Article{Coquand:Huet,
author = {Thierry Coquand and Gérard Huet},
title = {The Calculus of Constructions},
journal = {Information and Computation},
year = {1988},
volume = {76},
}
@INcollection{Coquand:metamathematical,
author = "Thierry Coquand",
title = "Metamathematical Investigations on a Calculus of Constructions",
booktitle="Logic and Computer Science",
year = {1990},
editor="P. Odifreddi",
publisher = "Academic Press",
}
@Misc{coqrefman,
title = {The {C}oq reference manual},
author={{C}oq {D}evelopment Team},
note= {LogiCal Project, \texttt{http://coq.inria.fr/}}
}
@Misc{coqsite,
author= {{C}oq {D}evelopment Team},
title = {The \emph{Coq} proof assistant},
note = {Documentation, system download. {C}ontact: \texttt{http://coq.inria.fr/}}
}
@Misc{Booksite,
author = {Yves Bertot and Pierre Cast\'eran},
title = {Coq'{A}rt: examples and exercises},
note = {\url{http://www.labri.fr/Perso/~casteran/CoqArt}}
}
@InProceedings{conor:motive,
author ="Conor McBride",
title = "Elimination with a motive",
booktitle = "Types for Proofs and Programs'2000",
volume = 2277,
pages = "197-217",
year = "2002",
}
|
