Experience Using Type Theory as a Foundation for Computer Science

unofficial copies [PDF], [PS]

by Robert L. Constable

Unpublished manuscript, Cornell University, 1996.


Computer science is emerging as one of the most enabling sciences of the century. While its physical basis lies in the applications of quantum mechanics -- producing the transistor and integrated circuits -- its impact rest equally on software abstractions -- a nonphysical basis. These abstractions are elaborated by mathematics, but they rest on a theoretical foundation which is not purely mathematical. This foundation is the subject of the article.