These notes comprise the lecture "Introduction to Type Theory" that I gave at the Alpha Lernet Summer School in Piriapolis, Uruguay in February 2008. The lecture was meant as an introduction to typed ¿-calculus for PhD. students that have some (but possibly not much) familiarity with logic or functional programming. The lecture consisted of 5 hours of lecturing, using a beamer presentation, the slides of which can be found at my homepage. I also handed out exercises, which are now integrated into these lecture notes. In the lecture, I attempted to give an introductory overview of type theory. The problem is: there are so many type systems and so many ways of defining them. Type systems are used in programming (languages) for various purposes: to be able to find simple mistakes (e.g. caused by typing mismatches) at compile time; to generate information about data to be used at runtime, .... But type systems are also used in theorem proving, in studying the the foundations of mathematics, in proof theory and in language theory.
|Title of host publication||Language Engineering and Rigorous Software Development (International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24-March 1, 2008, Revised Tutorial Lectures)|
|Editors||A. Bove, L. Soares Barbosa, A. Pardo, J. Sousa Pinto|
|Place of Publication||Berlin|
|Publication status||Published - 2009|
|Name||Lecture Notes in Computer Science|
Geuvers, J. H. (2009). Introduction to type theory. In A. Bove, L. Soares Barbosa, A. Pardo, & J. Sousa Pinto (Eds.), Language Engineering and Rigorous Software Development (International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24-March 1, 2008, Revised Tutorial Lectures) (pp. 1-56). (Lecture Notes in Computer Science; Vol. 5520). Berlin: Springer. https://doi.org/10.1007/978-3-642-03153-3_1