Search course

Use the search function to find more information about the study programmes and courses available at Chalmers. When there is a course homepage, a house symbol is shown that leads to this page.

Graduate courses

Departments' graduate courses for PhD-students.

​​​​
​​

Syllabus for

Academic year
DAT350 - Types for programs and proofs
Typer för bevis och program
 
Syllabus adopted 2019-02-07 by Head of Programme (or corresponding)
Owner: MPALG
7,5 Credits
Grading: TH - Pass with distinction (5), Pass with credit (4), Pass (3), Fail
Education cycle: Second-cycle
Major subject: Computer Science and Engineering, Software Engineering
Department: 37 - COMPUTER SCIENCE AND ENGINEERING


Teaching language: English
Application code: 02111
Open for exchange students: Yes
Block schedule: C

Module   Credit distribution   Examination dates
Sp1 Sp2 Sp3 Sp4 Summer course No Sp
0117 Oral examination 7,5c Grading: TH   7,5c    

In programs

MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 2 (elective)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 1 (compulsory elective)

Examiner:

Peter Dybjer

  Go to Course Homepage


Eligibility

General entry requirements for Master's level (second cycle)
Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.

Specific entry requirements

English 6 (or by other approved means with the equivalent proficiency level)
Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.

Course specific prerequisites

120 credits within computer science or mathematics or equivalent as well as basic knowledge in logic and functional programming. 

Aim

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 ntroduces 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 expose you to some practical applications of type-based technology in computer science.

Learning outcomes (after completion of the course the student should be able to)

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

Content

  •  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

Organisation

Lectures, exercise sessions, supervision.

Literature

  •  Types and Programming Languages by Benjamin Pierce, MIT Press
  •  Verified Functional Programming in Agda by Aaron Stump, Association for Computing Machinery and Morgan & Claypool

Examination including compulsory elements

  • Take home exam with supplementary oral exam for grades 4 and 5
  • Oral presentation of advanced topic or research result in type systems or of a programming project in the dependently typed language Agda


Page manager Published: Thu 04 Feb 2021.