Mentions légales du service

Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
Compare
user avatar
dates des prochaines séances: éviter le recouvrement
Gabriel Scherer authored
0913110c
History
user avatar 0913110c
History
Name Last commit Last update
agda
coq
exams
metaocaml/pottier
ocaml
overview
project
slides
tdtp
.gitignore
Makefile
README.OLD.md
README.md
README.md

Functional programming and type systems (2024-2025)

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 2024-2025. 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

  • (29/10/2024) Unary logical relations for simple types; (weak) normalisation of simply-typed λ-calculus (GS).

  • (05/11/2024) Unary logical relations for polymorphic types; (weak) normalisation of System F (GS).

    • (Same slides).

  • (12/11/2024) Binary logical relations and parametricity (GS).

    • (Same slides).

  • (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.

  • (10/12/2024) (Interlude.) Introduction to programming in Rust (JHJ)

Typed Programming

Programming with Resources in Rust

  • (04/02/2025) When the aliasing discipline is too strong (JHJ) (slides).
  • (11/02/2025) Practicing Rust.
  • (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, the teachers of this course, are planning to post a few internship proposals at some point during the fall.

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.

To find internships related to the topics of this course, you may wish to also contact our colleagues:

  • The Cambium team at Inria Paris. Keywords: program verification in separation logic (Iris; Osiris), programming language design and implementation (OCaml), proof assistants (Coq; MetaCoq), type systems, verified compilation, and more.
  • The PPS lab at IRIF, which includes the Picube team. Keywords: programming language design and implementation (OCaml), proof assistants (Coq), semantics, type theory, and more.
  • The Prosecco team at Inria Paris. Keywords: verification of security protocols (ProVerif; CryptoVerif; Squirrel), program verification, programming languages for the law (Catala), proof assistants (F*), software security, and more.
  • The Antique team at ENS Paris. Keywords: abstract interpretation, program analysis, analysis of biological systems, and more.
  • The Parkas team at ENS Paris. Keywords: synchronous programming languages, type systems, verified compilation, and more.
  • The Partout team at Inria Saclay. Keywords: connections between computation and deduction, proof theory, type theory, and more.
  • The Gallinette team at Inria Nantes. Keywords: formalized mathematics (Mathematical Components), proof assistants (Coq), type theory, and more.
  • The Toccata team at Inria Saclay. Keywords: automated deduction, program verification, and more.
  • The Epicure team at Inria Rennes. Keywords: automated deduction, program analysis, semantics, software security, verified compilation, and more.
  • The Pesto team at Inria Nancy. Keywords: electronic voting, verification of security protocols, verified compilation, and more.
  • The Stamp team at Inria Sophia. Keywords: formalized mathematics (Mathematical Components), proof assistants (Coq), verification of security protocols (EasyCrypt), and more.
  • The Cash team at ENS Lyon. Keywords: compilation, formalized mathematics (Mathematical Components), program analysis, semantics, type systems, verified compilation, and more.
  • The Camus team at Inria Strasbourg. Keywords: compilation, parallelism, program verification, semantics, and more.

We also have contacts abroad, mainly in Europe, North America, and Asia. If you would like to find an internship abroad, do not hesitate to talk to us.

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.