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 2018-02-13 by Head of Programme (or corresponding)
Owner: MPALG
7,5 Credits
Grading: TH - Five, Four, Three, Fail
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: Yes
Block schedule: C

Course elements   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:


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

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


Published: Fri 18 Dec 2009. Modified: Mon 28 Nov 2016