Introduction to type theory

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

6 Citaten (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.
Originele taal-2Engels
TitelLanguage Engineering and Rigorous Software Development (International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24-March 1, 2008, Revised Tutorial Lectures)
RedacteurenA. Bove, L. Soares Barbosa, A. Pardo, J. Sousa Pinto
Plaats van productieBerlin
ISBN van geprinte versie978-3-642-03152-6
StatusGepubliceerd - 2009

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'Introduction to type theory'. Samen vormen ze een unieke vingerafdruk.

Citeer dit