The Nuprl Open Logical Environment. - Stuart F. Allen; Robert L. Constable; Richard Eaton; Christoph Kreitz; Lori Lorigo (CADE, 2000)

MetaPRL - A Modular Logical Environment. - Jason Hickey; Aleksey Nogin; Robert L. Constable; Brian E. Aydemir; Eli Barzilay; Yegor Bryukhov; Richard Eaton; Adam Granicz; Alexei Kopylov; Christoph Kreitz; Vladimir Krupski; Lori Lorigo; et al. (TPHOLs, 2003)

A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. - Lori Lorigo; Jon M. Kleinberg; Richard Eaton; Robert L. Constable (MKM, 2004)

Innovations in computational type theory using Nuprl. - Stuart F. Allen; Mark Bickford; Robert L. Constable; Richard Eaton; Christoph Kreitz; Lori Lorigo; E. Moran (J. Appl. Log., 2006)