Implementing mathematics with the Nuprl proof development system. - Robert L. Constable; Stuart F. Allen; Mark Bromley; Rance Cleaveland; J. F. Cremer; Robert Harper 001; Douglas J. Howe; Todd B. Knoblock; Nax Paul Mendler; Prakash Panangaden; James T. Sasaki; Scott F. Smith 001 (Prentice Hall, 1986)

A Non-Type-Theoretic Semantics for Type-Theoretic Language. - Stuart F. Allen (1987)

The Semantics of Reflected Proof - Stuart F. Allen; Robert L. Constable; Douglas J. Howe; William E. Aitken (LICS, 1990)

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

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)