Preuves et programmes

Preuves et programmes

Ce cours est offert au second semestre du M1.

Contenu du cours :

Raisonner et programmer sont les deux côtés d’une même pièce.

L’épine dorsale de cette relation est la découverte d’une correspondance très forte entre des énoncés simples (calcul propositionnel) et des termes d’un modèle de calcul (λ-calcul). C’est la correspondance de Curry-Howard (1980).

En 2006, suite aux travaux de Voevodsky sur l’univalence (basée sur la théorie de l’homotopie), une nouvelle révolution est en marche. qui permet désormais de *faire des mathématiques en programmant*.

C’est un sujet qu’aucun format de cours ne saurait prétendre couvrir sur un seul semestre. Mais tous les chemins commencent par un premier pas, et nous nous assurerons de maîtriser d’abord les notions les plus fondamentales. Le programme envisagé est le suivant :

  • La correspondance de Curry-Howard, cuite dans son jus.
  • Théories de types et avènement des assistants à la preuve.
  • Les éléments d’une refondation des mathématiques : état de l’Art.

Références bibliographiques :

Outre la page de WikiPedia pour les impatients (https://fr.wikipedia.org/wiki/Correspondance_de_Curry-Howard) :

  • Intuitionistic Type Theory. P. Martin-Löf. 1980.
  • Proofs and Types. J.-Y. Girard, Y. Lafont, P. Taylor. 1987.
  • Lambda-calcul : types and modèles. J.-L. Krivine. 1990.
  • Homotopy Type Theory. Collectif. http://homotopytypetheory.org/book/.

Plus en suivant ce lien : https://perso.ens-lyon.fr/philippe.audebaud/PnP/

Géométrie computationnelle et images digitales

Image processing, digital and computational geometry

Course offered in the second semester of M1.

Objectives of the course:

The objective of this course is to introduce fundamental notions of image processing, digital geometry and computational geometry.  The first lectures will be dedicated to image processing (filtering, smoothing, morphological mathematics, ..) and shape representation. Then, we will focus on theoretical and algorithmic issues involved in the analysis of digital shapes. During this analysis of  digital geometry processing tools, we will have to present and integrate some tools from various fields: discrete mathematics, combinatorics, arithmetics, computational geometry, ..

Course contents:

  • Image/Shape representation
  • Image processing (filtering, segmentation)
  • Digital Geometry for shape analysis
  • Computational geometry and data structures
  • Requirements: basic notions of algorithmics

References:

  • Géométrie discrète et images numériques, D. Coeurjolly, A. Montanvert and J.-M. Chassery, Ouvrage collectif, Traité IC2, Hermès, 416 pages, 2007
  • Digital Geometry: Geometric Methods for Digital Picture Analysis, Reihnard Klette, Azriel Rosenfeld, Morgan Kaufmann, 2004
  • Computational Geometry: Algorithms and Applications, Mark de Berg, TU Eindhoven (the Netherlands) Otfried Cheong, KAIST (Korea),Marc van Kreveld, Mark Overmars, Utrecht University (the Netherlands), Springer-Verlag

Complexité algorithmique

Computational Complexity

Course offered in the second semester of M1.

Overview of the course:

Computational complexity aims to classify computational problems depending on the resources they need. One
studies various modes of computation such as deterministic, randomized, nondeterministic or quantum and compares
resources such as time or space needed to solve algorithmic problems. The objective of this course is to give a
broad understanding of the notions used to classify computational problems. About half of the course is dedicated
to studying basic complexity classes defined using Turing machines. We introduce (or study deeper) notions that are
central in complexity theory: nondeterministic computation (e.g., the class NP), reductions between computational
problems (e.g., NP-completeness) and the technique of diagonalization (e.g., hierarchy theorems). We also study
randomized computation and computation using boolean circuits as well as their relation to basic complexity classes.
We conclude the course by studying the complexity of communication, i.e., trying to evaluate communication
bottlenecks to perform a given computational task between different parties.
Teaching in 2014: Omar Fawzi (lectures) and S ́ebastien Maulat (exercise classes)

Course objectives:

One can summarize the most important objectives of the course as follows.

  1. Understand the formal definitions for the basic complexity classes like L, NL, P, NP, coNP, PSPACE.
    Be familiar with nondeterministic computation and the polynomial hierarchy. Know about the inclusions and separations between these classes.
  2. Understand the notion of reduction between computational problems, and the notion of complete problem, e.g., SAT is NP-complete, PATH is NL-complete, TQBF is PSPACE-complete.
  3. Understand complexity classes defined using boolean circuits, and the notion of uniformity in computation. Know the relation to basic complexity classes.
  4. Understand complexity classes using randomized computations. Know the relation to basic complexity classes.
  5. Get a flavour for the power of interactive proofs.
  6. Be familiar with an important tool in theoretical computer science: communication complexity. Be able to reduce various problems to a communication complexity problem.