@inproceedings{DBLP:conf/tphol/Harrison09a,
author = {John Harrison},
title = {HOL Light: An Overview},
booktitle = {TPHOLs},
year = {2009},
pages = {60-66},
ee = {http://dx.doi.org/10.1007/978-3-642-03359-9_4},
crossref = {DBLP:conf/tphol/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tphol/2009,
editor = {Stefan Berghofer and
Tobias Nipkow and
Christian Urban and
Makarius Wenzel},
title = {Theorem Proving in Higher Order Logics, 22nd International
Conference, TPHOLs 2009, Munich, Germany, August 17-20,
2009. Proceedings},
booktitle = {TPHOLs},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5674},
year = {2009},
isbn = {978-3-642-03358-2},
ee = {http://dx.doi.org/10.1007/978-3-642-03359-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}