Course syllabus

Jump to today

This is a 7.5 pt course offered by the department of Computer Science and Engineering.

The course is given online.

News

The grades are now finalized.

Schedule

  • Lectures:
    • Thursdays 10.00 – 11.45 beginning on 3 September: Zoom link Password: 363478;
    • Mondays 13.15 – 15.00 beginning on 7 September. Zoom link Password: 615747.
  • Exercise sessions:
    • Mondays 15.15 – 17.00 beginning on 7 September (with the same Zoom link as for the Monday lecture). This will include Agda supervision and discussion of homework. These sessions are for everyone, but in order to get credit for homework you must be prepared to present your solutions in class.

Course plan

Plan for lectures, exercise sessions and homework

Files from the lectures will be uploaded under "Files" in the menu to the left.

Course purpose

The development of advanced type systems is an important aspect of modern programming language design. This course provides an introduction to this area. In particular it introduces dependent types, types which can depend on (be indexed by) variables of other types. For example, the type of vectors is indexed by its length. Dependent types are versatile. Through the Curry-Howard identification of propositions and types virtually any property of a program can be expressed using dependent types. The student will learn how to use an interactive programming system for a language with dependent types. The course is thus simultaneously an introduction to

  • functional programming with dependent types;
  • computer-assisted interactive proving in logical systems, including predicate logic;
  • proving the correctness of functional programs;
  • type systems and operational semantics for programming languages.

Each of these topics is supported by experimenting with the interactive proof system.

Prerequisites:

  • Functional programming (essential).
  • Basic knowledge of logic, including predicate logic.
  • Some knowledge about programming languages.

Course literature

Agda:

Learning objectives and syllabus

  • 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
  • How to use deduction formalisms to present type systems and operational semantics of programming languages.
  • This is an advanced course which prepares you for doing a master's thesis in the area. Here are some proposals, but there are many more possibilities. Please talk to Peter, Thierry, or Ulf if you are interested.

Link to the syllabus Chalmers
Link to the syllabus GU

Examination

Obligatory parts:

  • Take home exam: Tuesday 20 October 8.00 – Friday 23 October 12.00.
  • Presentation of advanced topic or of an Agda development. You should work in pairs and choose a topic no later than on Friday 18 September. Please register your topic on the wiki. You will also be opponents for one of the presentations. Here are some talk proposals. The presentations and opposition are graded and give max 4 pts together.
  • Oral exam. To get the grades 4 or 5 at Chalmers, and VG at GU, you need to take a short oral exam. This is not necessary for grade 3 at Chalmers and G at GU.

Optional parts:

  • Homework. Bonus points will be given to students who have handed in homework and been prepared to present it in class (max 4 x 3 pts).
  • Attendance at the presentations gives 1 point for each of the 3 presentation sessions.

Note that both homework and take home exam should be done individually. If we find out that people have helped each other or copied solutions, we will fail the whole course both for the helper and the helped.

Contact details

  • Teachers:
  • Course evaluators:
    • Oskar Eriksson, oskeri@student.chalmers.se
    • Maria Kokkou, kokkou@student.chalmers.se
    • Beatrice Vergani, vergani@student.chalmers.se
    • Qufei Wang, qufei@student.chalmers.se

 

Course summary:

Date Details Due