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: zoom link
    Password: 037888

Schedule

  • Lectures:
    • Thursdays 10.00 – 11.45 beginning on 2 September: 
    • Mondays 13.15 – 15.00 beginning on 6 September.
  • Exercise sessions:
    • Mondays 15.15 – 17.00 beginning on 6 September. 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 and exercise sessions

 

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 Thierry, or Ulf if you are interested.

Link to the syllabus Chalmers
Link to the syllabus GU

Examination

Obligatory parts:

  • Take home exam: Tuesday 19 October 8.00 – Friday 22 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 17 September. Sign up on the presentation wiki page, which also contains a list of topic suggestions. You will also be opponents for one of the presentations. 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 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

 Course evaluators:   

  • Johan Ek  ekjoh@student.chalmers.se
  • Jakob Frykmer  frjakob@student.chalmers.se
  • Erik Ljungdahl   ljerik@student.chalmers.se
  • Lisa Snäll   lisasn@student.chalmers.se
  • Sam Sohrabpour   sosam@student.chalmers.se

 Teachers:

    • Thierry Coquand,   coquand@chalmers.se
    • Ulf Norell,   ulf.norell@cse.gu.se      

Course summary:

Date Details Due