Introduction to type theory

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationLanguage Engineering and Rigorous Software Development (International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24-March 1, 2008, Revised Tutorial Lectures)
EditorsA. Bove, L. Soares Barbosa, A. Pardo, J. Sousa Pinto
Place of PublicationBerlin
ISBN (Print)978-3-642-03152-6
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Introduction to type theory'. Together they form a unique fingerprint.

Cite this