Writing Programs that Construct Proofs. - Robert L. Constable; Todd B. Knoblock; Joseph L. Bates (J. Autom. Reason., 1985)

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)

Formalized Metareasoning in Type Theory - Todd B. Knoblock; Robert L. Constable (LICS, 1986)

Metamathematical Extensibility in Type Theory. - Todd B. Knoblock (1988)

Specializing shaders. - Brian K. Guenter; Todd B. Knoblock; Erik Ruf (SIGGRAPH, 1995)

Data Specialization. - Todd B. Knoblock; Erik Ruf (PLDI, 1996)

Operating System Directions for the Next Millennium. - William J. Bolosky; Richard Draves; Robert P. Fitzgerald; Christopher W. Fraser; Michael B. Jones; Todd B. Knoblock; Richard F. Rashid (Workshop on Hot Topics in Operating Systems, 1997)

Marmot: an optimizing compiler for Java. - Robert P. Fitzgerald; Todd B. Knoblock; Erik Ruf; Bjarne Steensgaard; David Tarditi (Softw. Pract. Exp., 2000)

Type elaboration and subtype completion for Java bytecode. - Todd B. Knoblock; Jakob Rehof (ACM Trans. Program. Lang. Syst., 2001)