main.bib

@Misc{FourColNot,
author = {Georges Gonthier},
title = {Notation of the {F}our {C}olour {T}heorem proof},
note = {Available at \\ \url{http://research.microsoft.com/~gonthier/4colnotations.pdf}}
}


@TECHREPORT{rt_sylow,
  AUTHOR = {Laurence Rideau and Laurent Théry},
  TITLE = {{F}ormalising {S}ylow's theorems in {C}oq},
  YEAR = 2006,
  INSTITUTION = {INRIA},
  NUMBER = {0327}
}

@misc{4color,
author = "Georges Gonthier",
title = "A computer-checked proof of the four-colour theorem",
type="Preprint",
note="Available at \url{http://research.microsoft.com/~gonthier/4colproof.pdf}"
}

@misc{ssr,
author = "Georges Gonthier",
title = "Notations of the Four Colour Theorem proof",
type="Preprint",
note="Available at \\ \url{http://research.microsoft.com/~gonthier/4colnotations.pdf}"
}



@Manual{Coq:manual,
  title =        {The Coq proof assistant reference manual},
  author =       {\mbox{The Coq development team}},
  organization = {LogiCal Project},
  note =         {Version 8.1},
  year =         {2007},
  url =          "http://coq.inria.fr"
}


@InProceedings{tphols07,
  author = 	 {Georges Gonthier and Assia Mahboubi and Laurence Rideau and Enrico Tassi and Laurent Thery},
  title = 	 {A modular formalisation of finite group theory},
  booktitle = {Proceedings of TPHOLs 2007},
  year = 	 {2007},
  series = 	 {LNCS},
  month = 	 {to appear},
}