Le cours consiste pour une grande partie en un projet de programmation. Les élèves développent en binôme un programme permettant soit d'exécuter d'autres programmes, soit de faire des raisonnements logiques. Le langage de programmation est OCaml. Des éléments de programmation fonctionnelle avancée sont abordés à l'occasion du développement du code.
Une partie du cours (environ 1/3) prend la forme de cours+TDs. On y traite de lambda-calcul, de typage, et de liens avec la théorie de la démonstration (correspondance de Curry-Howard).