Mentions légales du service

Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
Blame Permalink
README.md 10.45 KiB

Functional programming and type systems (2023-2024)

This page supplements the official page of MPRI 2-4.

This course presents the principles, formalisms, and mathematical techniques that underlie many of today's typed programming languages, including OCaml, Haskell, and Rust. Here are some introductory slides.

The course is taught by Pierre-Evariste Dagand (PED), Jacques-Henri Jourdan (JHJ), François Pottier (FP) (head), and Gabriel Scherer (GS).

The content of the course is partly renewed in 2023-2024. In particular, we will teach both syntactic and semantic proofs of type soundness, place more emphasis on logical relations, including logical relations in Iris, and present two distinct algorithmic approaches to type inference.

Didier Rémy's slides and lecture notes, from an earlier version of the course, are still available and can serve as a useful reference.

Location and Schedule

The lectures take place at University of Paris, Bâtiment Sophie Germain, in room 1002.

They are scheduled on Tuesdays from 12:45 to 15:30. There is a 15-minute break in the middle of each lecture, so each lecture lasts 2h30.

Syllabus and Time Table

The syllabus is organized in four main segments of five lectures each.

Operational Semantics, Type Systems, and Program Transformations

Semantic Proofs of Type Soundness and Logical Relations

  • (22/10/2024) Semantic interpretation of types: unary logical relations (GS).
  • (29/10/2024) Binary logical relations and parametricity (GS).
    • (same slides)
  • (05/11/2024) Mutable state and the value restriction (GS).
  • (12/11/2024) Strong normalization for System F in Coq (GS).
  • (19/11/2024) Semantic type soundness for System F with mutable state in Coq/Iris (JHJ).
  • (26/11/2024) mid-term exam, in the usual room and at the usual time, from 12:45 to 15:30, without a break. The duration of the exam is 2h45.

Typed Programming

Programming with Resources in Rust

  • (28/01/2025) Introduction to Rust programming (JHJ) (slides).
  • (04/02/2025) When the aliasing discipline is too strong (JHJ) (slides).
  • (11/02/2025) Multi-threading (JHJ) (slides).
  • (18/02/2025) Metatheory of Rust's type system (JHJ) (slides).
  • (25/02/2025) Exercise session (GS).
  • (04/03/2025) break
  • (11/03/2025) final exam

Evaluation of the course

Two written exams and one programming project are used to evaluate the students.

The mid-term exam will take place on 26/11/2024.

The final exam will take place on 11/03/2025.

The exam takes place in the usual room and at the usual time, from 12:45 to 15:30, without a break. The duration of the exam is 2h45.

Only printed course notes and hand-written notes are allowed during the mid-term and final exams. Electronic devices are not allowed.

Although the course evolves over time, you are encouraged to have a look at the previous exams and their solutions:

Programming Project

Programming is an important part of the course. We give a mandatory programming project, which counts for about a third of the final grade.

Research Internship Proposals

We are planning to post a few internship proposals at some point during the fall or winter.

The internship offers posted by the Prosecco team at Inria Paris are also relevant.

Please do not hesitate to talk to us (during the break or at the end of each lecture), to contact us by email, or to visit us at our offices.

See also the official list of internship offers at MPRI.

Recommended software

Coq

Please install opam first. A recent version is recommended (at the time of writing, 2.1.5). If you have installed it already, skip this step.

Then, install OCaml 4.12.0, Coq 8.13.2, and AutoSubst by executing this script. This script does not destroy your existing installation of OCaml and Coq. It creates a new "switch" named mpri24 and installs appropriate versions of OCaml, Coq, and AutoSubst in it. You can activate these versions with the following commands:

  ORIGINAL=$(opam switch show)
  opam switch mpri24
  eval "$(opam config env)"

and return to your original working environment with the following command:

  opam switch "$ORIGINAL"
  eval "$(opam config env)"

In order to use Coq inside emacs, ProofGeneral is highly recommended. Here is a suggested installation script.

If desired, ProofGeneral can be further customized.

Rust

In order to participate to the hands-on exercises on Rust, please install the following tools:

  • The Rust compiler (version 1.41 or newer)
  • The Cargo package manager (any compatible version)

Installation should be easy on any recent Linux distribution using the system's package manager. An alternative is to follow these instructions.

In order to test the installation, the students are asked to use the Rust compiler on the following program:

fn main() {
  let mut f = |x : i32| x;
  let _r : &mut dyn Fn(i32) -> i32 = &mut f;
  println!("{}", f(42))
}

If the compiler is correctly installed, then the command rustc test.rs should produce an executable.

Recommended Reading

Types and Programming Languages, Benjamin C. Pierce, MIT Press, 2002.

Advanced Topics in Types and Programming Languages, edited by Benjamin C. Pierce, MIT Press, 2005.

Practical Foundations for Programming Languages, Second Edition, Robert Harper, Cambridge University Press, 2016.