@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",
}