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

Authors: 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}
  }