Theory of Types and Programming Languages

Staff

Documents

Assignments

Project 1 - The NB Language

Project 2 - Untyped Lambda Calculus

Project 3 - Simply Typed Lambda Calculus

Project 4 - STLC Extensions

Project 5 - STLC with Type Reconstruction

Description

This course studies types and programming languages from a type-theoretic perspective. Starting from lambda calculus, the foundation of functional programming languages, we see how to design gradually more advanced type systems following the motto “Well-typed programs do not go wrong”, meaning that types should guard us, at compilation time, from wide classes of runtime errors. Taking this principle to the extreme, we see how dependent type systems let us prove nontrivial properties of our programs, and how they relate to mathematical logic in a fundamental way.

The knowledge acquired in this course has many practical applications in software engineering and computer science. It will sharpen the student’s understanding of static types in modern programming languages, as well as their ability to construct correct and reliable programs.

Topics covered include lambda calculus, operational semantics, type systems, programming language theory and metatheory.

Announcements

Announcements about the course will be made through Canvas at canvas.ust.hk/courses/42319/announcements.

Lecture notes and pen & paper session exercises are available in documents section.

Grading

Each enrolled student will receive a grade based on their results for the projects and the final exam. The relative importance of each part is: 30% for projects, 30% for the midterm exam, and 40% for the final exam.

Cheating

Sharing ideas is very recommended. However, plagiarizing code as part of a project will not be tolerated — whatever the source. In particular, you are not allowed to publish your projects in public repositories at GitHub/Bitbucket/… or to use solutions published by others.

In case of cheating, you will receive the grade “NA” (not acquired, zero) for the concerned project or exam, or for the whole course. You may furthermore be denounced and punished in accordance with the Academic Honor Code and Academic Integrity. If you are in any fashion worried about this, speak with an assistant.