Various documents and links related to administrative matters for M1 students, year 2024-2025.
These lectures introduce the Curry-Howard correspondence between proofs and programs, illustrating some of its key benefits.
We present the natural deduction system for both intuitionistic and classical logic, discussing the properties and limitations of these systems.
Furthermore, we establish a correspondence with the simply typed Lambda-Calculus and some of its extensions, such as the Lambda Mu-Calculus for classical natural deduction and System F for second-order propositional logic.
We will also prove some theorems that highlight the elegance of this correspondence, including the normalization and the parametricity theorems for System F.
Computer Algebra is the art of using a computer to perform exact mathematical computations. The aim of this course is to cover the fundamental algorithms of this field (from the Fast Fourier Transform to Gröbner bases), while providing the students with a practical familiarity with its uses and applications through tutorials using Maple. After this course, no student will think of using pen-and-paper for long mathematical derivations.