Course syllabus adopted 2021-02-26 by Head of Programme (or corresponding).
Overview
- Swedish nameTyper för bevis och program
- CodeDAT350
- Credits7.5 Credits
- OwnerMPALG
- Education cycleSecond-cycle
- Main field of studyComputer Science and Engineering, Software Engineering
- DepartmentCOMPUTER SCIENCE AND ENGINEERING
- GradingTH - Pass with distinction (5), Pass with credit (4), Pass (3), Fail
Course round 1
- Teaching language English
- Application code 02113
- Block schedule
- Open for exchange studentsYes
Credit distribution
Module | Sp1 | Sp2 | Sp3 | Sp4 | Summer | Not Sp | Examination dates |
|---|---|---|---|---|---|---|---|
| 0117 Oral examination 7.5 c Grading: TH | 7.5 c | 0 c | 0 c | 0 c | 0 c | 0 c |
In programmes
- MPALG - COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 1 (compulsory elective)
- MPALG - COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 2 (elective)
Examiner
Thierry Coquand- Full Professor, Computing Science, Computer Science and Engineering
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.