Skip to content

leo-leesco/fun

BranchesTags

Repository files navigation

Functional programming and type systems (FUN) (2025-2026)

This is the main home page of the course Functional programming and type systems, also known under the code names 2.4 and FUN. The course also has a shorter official page on MPRI's site.

Optional: please take a few minutes to fill our unofficial registration form. This helps us know you better and faster.

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 Jacques-Henri Jourdan (JHJ), François Pottier (FP) (head), Gabriel Scherer (GS), and Yannick Zakowski (YZ). This year, one lecture will be given by Didier Rémy (DR).

The content of the course is partly renewed in 2025-2026. In particular, we will go deeper into monads, with two new lectures on interaction trees and modular monadic semantics for programming languages. Also, the last part of the course includes a new lecture on translating Rust to purely functional code.

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 1004.

They are scheduled on Wednesdays 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 roughly comparable sizes. The title of each segment (below) is a hyperlink; click it to obtain a more detailed description of each segment.

Syntax, Operational Semantics, and Type Systems

Semantic Proofs of Type Soundness and Logical Relations

  • (12/11/2025) Unary logical relations for simple types; (weak) normalisation of simply-typed λ-calculus; unary logical relations for polymorphic types; (weak) normalisation of System F (GS).

  • (19/11/2025) Binary logical relations and parametricity; logical relations for mutable state, with step-indexing (GS).

  • (26/11/2025) mid-term exam, in rooms 1002 and 1004 and at the usual time, from 12:45 to 15:30, without a break. The duration of the exam is 2h45.

  • (03/12/2025) Break

Modular Programming and Modular Semantics

Programming with Resources in Rust

  • (28/01/2026) Introduction to programming in Rust (JHJ).

  • (04/02/2026) Rust generics and traits (JHJ).

  • (11/02/2026) Practicing Rust; concurrency (JHJ).

  • (18/02/2026) Metatheory of Rust's type system; a semantic interpretation of types (JHJ).

  • (25/02/2026) Translating Rust to purely functional code (JHJ).

  • (04/03/2026) break

  • (11/03/2026) final 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.

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

The deadline for the programming project is 27/02/2026.

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

The coefficients are:

  • either mid-term exam: 3 and final exam: 4 or mid-term exam: 4 and final exam: 3 (whichever is more advantageous for each student);
  • programming project: 3.

Thus, the sum of the coefficients is 10.

The exams take 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.

The project for the year 2025-2026 should be made available in late November 2025.

The deadline is: Friday, February 27, 2026, at 23:59.

Research Internship Proposals

We, the teachers of this course, usually post a few internship offers 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. 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.

About

Functional programming and type systems

gitlab.inria.fr/fpottier/mpri-2.4-public.git

Resources

Readme
Activity

Stars

1 star

Watchers

0 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Contributors 9

Languages