Department of Information and Computing Sciences

Departement Informatica Onderwijs
Bachelor Informatica Informatiekunde Kunstmatige intelligentie Master Computing Science Game&Media Technology Artifical Intelligence Human Computer Interaction Business Informatics

Onderwijs Informatica en Informatiekunde

Vak-informatie Informatica en Informatiekunde

Theory of programming and types

Onderwijs:Het vak INFOMTPT wordt in 2020/2021 niet aangeboden.
Nota bene:Er is geen recente vakbeschrijving beschikbaar.
Onderstaande tekst is een oude vakbeschrijving uit collegejaar 2013/2014
Inhoud:After completing this course, you will be able to:
1 program in a dependently typed programming language such as Agda.
2 prove properties of programs and systems using a dependently typed programming language such as Agda.
3 write and design datatype generic programs, for example by using a universe construction in Agda, but also by using fixed-points.
4 design a type system for a programming language.
5 formulate and prove properties of such a type system.
6 read, present, and use results from papers from the important conferences in the field, such as the Symposium on Principles of Programming Languages (POPL), and International Conference of Functional Programming (ICFP). This course will prepare you to to contribute to research in this area.
Literatuur:Kan veranderen!
Papers to be distributed at the course.
Werkvorm:Lectures, homework exercise sets, student presentations, research projects.
Toetsvorm: A. Exercise sets - 3 sets on lecture material (1,2,3,5) (40%) B. Research paper presentation - present research article with an analysis (6) (20%) C. Research project - work in a team to formulate and solve a research problem, present results in a presentation and report (4,5,6) (40%)
Inspanningsverplichting voor aanvullende toets:Om aan de aanvullende toets te mogen meedoen moet de oorspronkelijke uitslag minstens 4 zijn.
Beschrijving:In this course we will study an important research method in the world of programming, programming languages and types. We will discuss how to set up programming languages and type systems, how to formally prove properties of languages, semantics and type systems in a dependently typed programming language. Note that there is some overlap with the seminar on Dependently Typed Programming and the course on Generic Programming. If you have completed either of these courses, please contact the lecturers before enrolling.