Types for Programs and Proofs

Utbildningsfakta

Kod: DIT235

The development of powerful type systems is an important aspect of modern programming language design. This course provides an introduction to this area. In particular it introduces the notion of dependent type, a type which can depend on (is indexed by) values of another type, for example, the type of vectors indexed by its length. Dependent types are versatile. Through the Curry-Howard identification of proposition and types virtually any property of a program can be expressed using dependent types. The aim of the course is to give a solid and broad foundation in type systems for programming languages, and also give examples of type-based technologies in computer science. - introduction to lambda calculus and simple type theory - introduction to operational semantics and type systems - dependent type theory - the Curry-Howard identification of propositions as types - programming in Agda, a proof assistant - presentation of advanced topics in type systems

Behörighet

To be eligible to the course, the student should have successfully completed 120 credits of studies in computer science or mathematics, or equivalent. Specifically, a successfully completed 7.5 credit course in discrete mathematics (e.g., DIT980 Discrete Mathematics for Computer Scientists, or equivalent) and a successfully completed 7,5 credit course in functional programming (e.g. DIT143 Functional Programming, or equivalent is required. Applicants must prove knowledge of English: English 6/English level 2 or the equivalent level of an internationally recognized test, for example TOEFL, IELTS.

Utbildningstillfällen

Varje tillfälle har egna datum och villkor. Avslutade tillfällen behålls som historik och innebär inte att en ny ansökan är öppen.

• Types for Programs and Proofs

  University of Gothenburg

  GÖTEBORG

  Startdatum: 31 augusti 2026

  Slutdatum: 1 november 2026

  Studietakt: 50 %