The main contributions were in developing type systems that allow both partial and total functions to be typed in a single type theory.
S. Smith, Hybrid Partial-Total Type Theory. International Journal of Foundations of Computer Science volume 6, 235-263, 1995.
This paper is a simplified version of the results in my PhD thesis.
S. Smith, Reflective Semantics of Constructive Type Theory. Constructivity in Computer Science, Springer-Verlag LNCS 613, 1992.
S. Smith, Extracting Recursive Programs in Type Theory. AMAST 1991, Springer-Verlag Workshops in Computing Series.
Computational foundations of basic recursive function theory. Theoretical Computer Science, December 1993 (with Robert Constable).
Implementing Mathematics with the Nuprl Proof Development System. Englewood Cliffs: Prentice Hall, 1986 (with Robert Constable, et. al.).