@string{itp = "International Conference on Interactive Theorem Proving"}
@string{tphols = "International Conference on Theorem Proving in Higher Order Logics"}
@string{proc = "Proceedings of the"}
@string{lncs = "Lecture Notes in Computer Science"}
@string{access = "Last access:"}
@string{avail = "Available at:"}

@Misc{debruijn2003,
  author = 	 {N.G. de Bruijn},
  title = 	 {Memories of the {AUTOMATH} project},
  howpublished = {Invited lecture at the Mathematics Knowledge Management Symposium 25--29 November 2003 Heriot-Watt University, Edinburgh, Scotland},
  month = 	 {Nov.},
  year = 	 {2003},
  note = 	 avail # { \url{http://www.win.tue.nl/automath/aboutautomath.htm} } # access # { 2014/08/21 }
}

@InProceedings{harrison2006ijcar,
  author = 	 {John Harrison},
  title = 	 {Towards Self-verification of {HOL} {Light}},
  booktitle = proc # { 3rd International Joint Conference on Automated Reasoning, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006},
  pages = 	 {177--191},
  year = 	 {2006},
  volume = 	 {4130},
  series = 	 lncs,
  publisher = {Springer}
}

@InProceedings{nipkow2006tame,
  author = 	 {Tobias Nipkow and Gertrud Bauer and Paula Schultz},
  title = 	 {Flyspeck {I}: Tame Graphs},
  booktitle = proc # { 3rd International Joint Conference on Automated Reasoning, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006},
  year = 	 {2006},
  volume = 	 {4130},
  series = 	 lncs,
  pages = 	 {21--35},
  publisher = {Springer}
}

@Article{hales2008ams,
  author = 	 {Thomas C. Hales},
  title = 	 {Formal Proof},
  journal = 	 {Notices of the American Mathematical Society},
  year = 	 {2008},
  volume = 	 {55},
  number = 	 {11},
  pages = 	 {1370--1380}
}

@InProceedings{winwood2009tphols,
  author = 	 {Simon Winwood and Gerwin Klein and Thomas Sewell and June Andronick and David Cock and Michael Norrish},
  title = 	 {Mind the Gap},
  booktitle = proc # { 22nd } # tphols # {, TPHOLs 2009, Munich, Germany, August 17--20, 2009},
  year = 	 {2009},
  volume = 	 {5674},
  series = 	 lncs,
  pages = 	 {500-515},
  publisher = {Springer}
}

@Article{asperti2009mscs,
  author = 	 {Andrea Asperti and Herman Geuvers and Raja Natarajan},
  title = 	 {Social processes, program verification and all that},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 {2009},
  volume = 	 {19},
  number = 	 {5},
  pages = 	 {877--896}
}

@InProceedings{proviola,
  author = 	 {Carst Tankink and Herman Geuvers and James McKinna and Freek Wiedijk},
  title = 	 {Proviola: {A} Tool for Proof Re-animation},
  booktitle = proc # { Conferences on Intelligent Computer Mathematics, CICM 2010,
(AICS 2010, Calculemus 2010, {MKM} 2010), Paris, France, July 5-10, 2010},
  year = 	 {2010},
  volume = 	 {6167},
  series = 	 lncs,
  pages = 	 {440--454},
  organization = {Springer}
}

@InProceedings{klein2010aplas,
  author = 	 {Gerwin Klein},
  title = 	 {From a Verified Kernel towards Verified Systems},
  booktitle = proc # { 8th Asian Symposium on Programming Languages and Systems, APLAS 2010, Shanghai, China, November 28--December 1, 2010},
  pages = 	 {21--33},
  year = {2010},
  volume = 	 {6461},
  series = 	 lncs,
  publisher = {Springer}
}

@Misc{hales2011,
  author = 	 {Thomas C. Hales},
  title = 	 {Lessons Learned from the Flyspeck Project},
  howpublished = {{I}nternational {S}pring {S}chool on {F}ormalization of {M}athematics ({MAP} 2012), {M}arch 12--16, 2012, {S}ophia {A}ntipolis, {F}rance},
  month = 	 {Mar.},
  year = 	 {2012},
  note = 	 avail # { \url{http://www-sop.inria.fr/manifestations/MapSpringSchool/contents/ThomasHales.pdf} } # access # { 2014/08/22}
}

@Misc{hales2013turing,
  author = 	 {Thomas C. Hales},
  title = 	 {Mathematics in the Age of the Turing Machine},
  howpublished = {arXiv:1302.2898v1 [math.HO]},
  month = 	 {Feb.},
  year = 	 {2013}
}

@InProceedings{bolignano2013itp,
  author = 	 {Dominique Bolignano},
  title = 	 {Applying Formal Methods in the Large},
  booktitle = proc # { 4th } # itp # {, ITP 2013, Rennes, France, July 22--26, 2013},
  pages = 	 {1},
  year = {2010},
  volume = 	 {7998},
  series = 	 lncs,
  publisher = {Springer}
}

@Misc{nipkow2014ihp,
  author = 	 {Tobias Nipkow},
  title = 	 {Tame graph enumeration in {Flyspeck}},
  howpublished = {Workshop on Formalization of Mathematics in Proof Assistants, Institut Henri Poincar\'e},
  month = 	 {May},
  year = 	 {2014},
  note = 	 {Oral presentation}
}

@Misc{wiedijk2014ihp,
  author = 	 {Freek Wiedijk},
  title = 	 {Formal proof done right},
  howpublished = {Workshop on Formalization of Mathematics in Proof Assistants, Institut Henri Poincar\'e},
  month = 	 {May},
  year = 	 {2014},
  note = 	 {Oral presentation}
}

@Misc{hales2014ihp,
  author = 	 {Thomas C. Hales},
  title = 	 {Solovyev's Formal Computations in {HOL} Light},
  howpublished = {Workshop on Formalization of Mathematics in Proof Assistants, Institut Henri Poincar\'e},
  month = 	 {May},
  year = 	 {2014},
  note = 	 {Oral presentation}
}