Search programme

​Use the search function to search amongst programmes at Chalmers. The study programme and the study programme syllabus relating to your studies are generally from the academic year you began your studies.

Syllabus for

Academic year
DAT350 - Types for programs and proofs
Typer för bevis och program
 
Syllabus adopted 2021-02-26 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: 02122
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:

Thierry Coquand

  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


The course examiner may assess individual students in other ways than what is stated above if there are special reasons for doing so, for example if a student has a decision from Chalmers on educational support due to disability.


Page manager Published: Mon 28 Nov 2016.