Types for Programs and Proofs

The course can be part of the following programmes:

1. Computer Science, Master's Programme (N2COS)
2. Computer Science, Bachelor's Programme (N1COS)

The course is a also a single-subject course at Gothenburg University.

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.

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

On successful completion of the course the student will be able to:

Knowledge and understanding

• describe several kinds of type systems, their underlying design principles, and their semantic foundation
• read and present a research topic in the area

Competence and skills

• program in a dependently typed functional programming language
• prove theorems in a dependently typed programming language using the propositions-as-types principle
• use deduction formalisms to present type systems and operational semantics of programming languages

Judgement and approach

• critically analyse type systems and prove properties about them

Lectures, exercise sessions, supervision.

Language of instruction: English

The course is examined by an oral presentation normally performed in pairs, and by an individual take home examination. In addition, to receive a higher grade than 3/Pass the student has to pass an individual oral examination.

The take home exam includes both theoretical problems and programming assignments. For the oral presentation, the student can select either a research paper or a chapter in the course book involving applications of type systems not covered in the lectures.

If the take-home exam is handed in too late it is failed. An oral examination is used as reexamination.

If a student who has been failed twice for the same examination element wishes to change examiner before the next examination session, such a request is to be granted unless there are specific reasons to the contrary (Chapter 6 Section 22 HF).

If a student has received a certificate of disability study support from the University of Gothenburg with a recommendation of adapted examination and/or adapted forms of assessment, an examiner may decide, if this is consistent with the course’s intended learning outcomes and provided that no unreasonable resources would be needed, to grant the student adapted examination and/or adapted forms of assessment.

If a course has been discontinued or undergone major changes, the student must be offered at least two examination sessions in addition to ordinary examination sessions. These sessions are to be spread over a period of at least one year but no more than two years after the course has been discontinued/changed. The same applies to placement and internship (VFU) except that this is restricted to only one further examination session.

If a student has been notified that they fulfil the requirements for being a student at Riksidrottsuniversitetet (RIU student), to combine elite sports activities with studies, the examiner is entitled to decide on adaptation of examinations if this is done in accordance with the Local rules regarding RIU students at the University of Gothenburg.

Sub-courses

1. Take home examination, 7.5 credits
   Grading scale: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U)

The grading scale comprises: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U).

The grade on the course is the same as the grade on the sub-course Take home examination.

The course is evaluated through meetings both during and after the course between teachers and student representatives. Further, an anonymous questionnaire is used to ensure written information. The outcome of the evaluations serves to improve the course by indication which parts could be added, improved, changed or removed.

Knowledge of Functional Programming is recommended, e.g., from the course DIT143 Functional Programming, or equivalent.

The course is a joint Chalmers-GU course.

The course replaces the course DIT233, 7.5 credits. The course cannot be included in a degree which contains DIT233. Neither can the course be included in a degree which is based on another degree in which the course DIT233 is included.