Na´ve Computational Type Theory -- Revision History

Constable, Robert L., Na´ve Computational Type Theory. Cornell University, 2002.
Revision Date Revision
2/11/03 Title was changed from "Naive Type Theory" to "Naive Computational Type Theory" per Bob. Now the title is the same as that of the former version published in Proof and System-Reliability (see 11/1/02 note below).
11/5/02 Typo corrected in Section 1, "Types and equality," under "Equality."

The first formula had read incorrectly:
      x=y mod(m) iff (x-y)=k [etc.]
It has now been corrected to:
      x=y mod(k) iff (x-y)=k [etc.]
11/1/02 "Naive Type Theory" is a revised version of R. Constable, "Naive Computational Type Theory," in H. Schwichtenberg & R. Steinbrueggen, eds., Proof and System-Reliability, NATO Science Series III, pp. 213-260, Kluwer Academic Publishers, 2002.
Back to Naive Computational Type Theory -- Preface page