Functional Projects

Instructor: Daniel Hirschkoff

Institution: ENS de Lyon

Year: 2024–2025

Main topics

  • Lambda calculus
  • Curry-Howard correspondence
  • Type theory
  • Proof theory

Description

The objective of this course is to implement an interpreter for the OCaml language (called Fouine) and a Rocq-like proof assistant (called Pieuvre) in OCaml. The majority of the time is spent implementing, although there is a theoretical section between both projects.

Projects

The projects are developped in groups of 2. I collaborated with Juliette Ponsonnet.

The pages for the projects can be found here : Fouine Pieuvre

Course chapters

  1. Pure lambda calculus, confluence
  2. Simple types for lambda calculus, strong normalization
  3. Dialogue with logic: proof theory
  4. Advanced type systems for programming