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