## Invited Paper: Experience using type theory as a foundation for computer science (at LICS 1995)

**Robert L. Constable**

### Abstract

Type theory is an elegant organisation of the fundamental principles of a foundational theory of computing, with theory taken in the sense of a scientific theory as well as a deductive theory. This theory generates a research programme. I examine the elements of this programme and assess progress. A large number of people world wide have been pursuing the type theory aspects of this research programme, so we can survey a large body of work created over a 20 year period for hints of success and failure and challenge. I first look at a few successes. Some of the applications we have attempted have not worked out as expected, and we don't know whether the fault lies with the type theory or elsewhere. I first describe a failure that is clearly not the type theory, but the state of the foundations of computational mathematics. Then we look at problems closer to the structure of modern type theories-problems suggested by the success of classical set theory.

### BibTeX

@InProceedings{Constable-Experienceusingtype, author = {Robert L. Constable}, title = {Experience using type theory as a foundation for computer science}, booktitle = {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)}, year = {1995}, month = {June}, pages = {266--279}, location = {San Diego, CA, USA}, note = {Invited Talk}, publisher = {IEEE Computer Society Press} }