Journal of Automated Reasoning, vol. 50, pp. 173-190 (2013).
@ARTICLE{harrison-pnt, author = "John Harrison", title = "The {HOL} {L}ight theory of Euclidean space", journal = "Journal of Automated Reasoning", year = 2013, volume = 50, pages = "173--190"}