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)

Extracting Efficient Programs From Constructive Proofs. - James T. Sasaki (1986)

Efficient Verified Programs in a Typed Theory with Mixed Constructivity. - James T. Sasaki (J. Log. Comput., 1995)

A Type Theory with Mixed Constructivity and Assignments. - James T. Sasaki (Log. J. IGPL, 1997)