Constructive Type Theory

Status

Inactive.

The main contributions were in developing type systems that allow both partial and total functions to be typed in a single type theory.

Publications

  • 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.).

Dissertations