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
DAT140 - Types for programs and proofs
 
Syllabus adopted 2015-02-13 by Head of Programme (or corresponding)
Owner: MPALG
7,5 Credits
Grading: TH - Five, Four, Three, Not passed
Education cycle: Second-cycle
Major subject: Computer Science and Engineering, Information Technology
Department: 37 - COMPUTER SCIENCE AND ENGINEERING


Teaching language: English
Open for exchange students
Block schedule: C

Course module   Credit distribution   Examination dates
Sp1 Sp2 Sp3 Sp4 Summer course No Sp
0108 Written and oral assignments 7,5c Grading: TH   7,5c    

In programs

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:

Professor  Peter Dybjer
Professor  Thierry Coquand



  Go to Course Homepage

Eligibility:


In order to be eligible for a second cycle course the applicant needs to fulfil the general and specific entry requirements of the programme that owns the course. (If the second cycle course is owned by a first cycle programme, second cycle entry requirements apply.)
Exemption from the eligibility requirement: Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling these requirements.

Course specific prerequisites

The requirement to the course is to have successfully completed a Bachelor degree within Computer Science or equivalent. The student needs to possess basic knowledge in logic and functional programming. This knowledge can be obtained from the courses Logic in computer science and Functional programming given at Chalmers or from courses with similar content.

Aim

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)

After completing the course the student should have a solid and broad foundation in type systems for programming languages. The student will be able to design, analyse, and implement type systems and also use them in different application areas. Moreover, the student will be able to work with an interactive programming and proof system using dependent types.

Content

Functional programming, constructive logic, simply typed lambda calculus, type safety, inductive definitions and proof techniques, dependent types, proof assistants based on type theory.

The course will also contain an introduction to programming with dependent types and Martin-Löf's constructive type theory. Examples will be given which illustrate the unity of Mathematics and programming in this theory.

Organisation

Lectures, exercise sessions, supervision.

Literature

See the course homepage.

Examination

The course is examined by homework, an oral presentation, and by a take home exam.

The homework and the take home exam includes both theoretical problems and programming assignments in Agda, an interactive programming and proof system using dependent types. The oral presentation is done in pairs, and 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. The presentation is judged both with respect to the quality of the slides and of the oral presentation.


Page manager Published: Thu 04 Feb 2021.