Master Mathématiques et applications, Parcours : Informatique et Mathématiques discrètes (IMD)

Tronc commun

• Algorithmique et complexité (SMACUA2L)

  Intervenants : Nadia Creignou, Victor Chepoi

  Complexité :

  • Mise à niveau : calculabilité et décidabilité : machines de Turing, thèse de Church, notion de réduction
  • Les classes P, NP et au delà : P, NP, problèmes fortement NP-complets, hierarchie polynomiale, compelxité en espace, complexité descriptive.
  • Approximation et complexité ; classes d'approximation, résultats de non approximabilité, réductions pour l'approximation et problèmes complets.
  • Complexité paramétrée : FPT et kernelisation.
  • Éventuellement : complexité du comptage.

  Algorithmes:

  • Mise à niveau:
    1. Algorithmes de graphes: parcours, plus court chemin, arbres couvrants, flots
    2. programmation linéaire: méthode simplex, dualité, modélisation des problèmes NP complèts comme programmes linéaires en nombres entiers;
  • Plutôt P:
    1. Diviser-pour-règner: multiplications des entiers, élément k minimal, transformée rapide de Fourier;
    2. Programmation dynamique: distance d'édition et distance d'édition en espace linéaire, structure secondaire d'un ARN, stable max d'un arbre;
    3. Algorithmes gloutons. Matroïdes et algorithmes gloutons. Axiomatiques des matroïdes par bases, circuits, fonction de rang;
    4. Méthode locale: recuit simulé, configurations stables dans les réseaux de Hopfield, mariage stable, coupe maximum d'un graphe (algo facteur 2);
  • Plutôt NPC:
    1. Algorithmes d'approximation: facteur 2 pour VERTEX COVER facteur 2 et 4/3 pour ordonnancement des tâches, facteur 2 NextFit et 3/2 FirstFitDecreasing pour BinPacking. FPTAS pour le  Sac à Dos. PTAS pour ordonnancement des tâches.
    2. Largeur arborescente d'un graphe. Algorithmes à paramètres exactspour VERTEX COVER dans des graphes de largeur arborescente bornée.
    3. PSPACE: QSAT et Planification ((s,t)-Reachability) sont dans PSPACE (theoreme de  Savitch);
    4. Randomisation (rappels): analyse de la complexité en esperance pour Quicksort, algorithmes d'approximation pour CoupeMax et MaxSAT (par randomisation et programmation linéaire). Dérandomisation pour MaxSAT. Comptage approximatif et  schéma d'approximation randomise FPTRAS pour  les comptage #DNF.
  • Thèmes complémentaires:
    • Algorithmes géométriques: diagrammes de Voronoi par diviser pour règner et par balayage, triangulations de Delaunay méthode incrémentale randomisée;
    • Algorithmes en ligne et compétitivité. Analyse en compétitivité de la k-pagination, le list accessing problem, et les k serveurs sur un arbre;
    • VC-dimension et le théorème des epsilon-réseaux et le PAC learning.

• Logique et automates(SMACUA3L & SMADU32L)

  Intervenants : Pierre-Alain Reynier, Lionel Vaux, Laurent Regnier

  Logique

  • Mise à niveau :
    • Formules : calcul propositionnel, calcul des prédicats, modèles
    • Preuves : règles et arbres de déduction, résultats de correction, complétude et incomplétude
  • Logiques du second ordre
  • Calcul des séquents
  • Théorème d’élimination des coupures et applications.
  • Lambda-calcul, lambda-calcul typé, correspondance de Curry-Howard
  • Système F

  Automates

  • Mise à niveau : Automates finis et langages réguliers
  • Logiques FO et MSO sur les mots finis et infinis
  • Théorème de Büchi : équivalence automates finis et logique MSO
  • Automates de Büchi : propriétés de clôture, de décision, lien avec MSO
  • Automates d’arbres : propriétés de clôture, de décision, logique MSO sur les arbres
  • Logiques temporelles (LTL, CTL), application au model-checking
  • Automates alternants : équivalence avec les automates finis, application à LTL

• Modèles de calcul, systèmes dynamiques, théorie algorithmique des nombres (SMACUA4L)

  Intervenants : Pierre Guillon, Kevin Perrot, Sylvain Séné, Guillaume Theyssier, David Kohel

  • Modèles de calcul, systèmes dynamiques (voir le chapitre 1 du cours de l'EJCIM 2017 pour plus de précisions sur la partie automates cellulaires/pavage)
    • Automates cellulaires : équivalence des définitions locale et topologique, réversibilité, théorème du jardin d'Éden et de l'équilibre, décidabilité de ces propriétés en 1D et indécidabilité en 2D.
    • Pavages par tuiles de Wang et sous-shifts (de type fini) : indécidabilité du domino problem, apériodicité, arécursivité.
    • Réseaux d'automates booléens : dynamique et structure, expressivité, théorème des points fixes, influence des modes de mise à jour (déterministes et non déterministes), théorèmes de convergence au regard des cycles d'interactions.
  • Théorie algorithmique des nombres:

    On introduit la complexité algorithmique à travers des problèmes et questions de la théorie (élémentaire) des nombres, motivés par la cryptographie : comment faire des opérations de base (multiplication des entiers, exponentiation modulaire) nécessaires pour (l'implémentation dans un ordinateur) les corps finis, les problèmes algorithmiquement difficiles -- les logarithmes discrets et la factorisation -- sur lesquels reposent la sécurité des cryptosystèmes, et les meilleurs algorithmes connus pour les résoudre.

    Dans le cadre spécifique de la cryptographie, l'objectif est de comprendre que la sécurité (des cryptosystèmes à clef publique) se repose sur l'écart entre la complexité des algorithmes à temps polynômial et des algorithmes à temps soit exponentiel, soit sous-exponentiel. Dans le cadre général, les étudiants acquièrent des connaissances, appréciation, et capacité d'évaluer la complexité des problèmes algorithmiques qu'ils rencontrent dans la vie quotidienne d'un mathématicien.

Mathématiques discrètes

• Théorie de l'information, algorithmique, cryptographie et codage (SMACUD6L)

  Intervenants : Stéphane Ballet, Alexis Bonnecaze, David Kohel

  Les outils mathématiques utilisés en cryptographie et codage évolue pour s'adapter à la puissance des ordinateurs et des services demandés.  C'est particulièrement vrai en ce qui concerne la cryptographie asymétrique dont la sécurité repose sur la difficulté de résoudre certains problèmes. L'introduction des courbes elliptiques a permis de réduire la taille des clés tout en gardant un niveau de sécurité identique. Les pairings ont permis d'obtenir de nouvelles primitives cryptographiques et ont en particulier amené la cryptographie basée sur l'identité. Le futur est actuellement principalement incarné par des outils basés sur des propriétés de la physique quantique.

  L'objectif de ce cours est de présenter ces outils théoriques ainsi que leurs applications en cryptographie et codage, et de s'intéresser à certaines implémentations en langages Sage, Magma et C.

  Plan du cours :

  • Introduction
  • Problèmes difficiles (DLP, factorisation, CDH, DDH, etc)
  • Courbes elliptiques pour la cryptographie
  • Pairings et IDBased crypto
  • Introduction à la cryptographie post-quantique
  • Introduction au codes correcteurs d'erreurs quantiques

• Modèles de calcul naturel (SMACUA6L)

  Intervenants : Giuseppe Di Molfetta, Kévin Perrot, Enrico Porreca, Sylvain Sené

  Cette UE vise à donner aux étudiants qui la suivent une "culture" dans le domaine du calcul naturel, à la frontière des mathématiques discrètes et de l'informatique (fondamentale). Nous y introduirons certains des principaux modèles classiques du domaine comme les automates cellulaires et plus largementles réseaux d'automates, ainsi que les piles de sable. Par ailleurs, une partie de cette UE visera à présenter les fondamentaux de l'informatique et de l'information quantiques. La présentation de ces différents domaines du calcul naturel permettra aussi d'établir des liens que les mathématiques discrètes et l'informatique entretiennent avec d'autres disciplines, comme la biologie et la physique.

• Topologie algèbrique discrète - topologie algorithmique (SMACUD1L)

  Intervenants :  Dimitri Ara, Alexandra Bac

  Introduction

  • Topologie algébrique : du continu au discret

  Les fondements

  • Espaces topologiques, complexes simpliciaux et cubiques
  • Bases du langage des catégories
  • Un peu d’algèbre homologique
  • Homologie singulière
  • Invariance par homotopie
  • Suite exacte de Mayer-Vietoris et calculs

  Homologie simpliciale et cubique

  • Esquisse de comparaison avec l’homologie singulière
  • Ouverture vers les groupes d’homotopie

  Vers la géométrie discrète :

  • Notions de géométrie discrète (objets binaires et leur topologie, complexes associés)

  Calcul de l’homologie singulière :

  • soit par des approches algébriques (forme normale de Smith)
  • soit approches combinatoires (théorie de Morse discrète)
  • soit en combinant les deux (homologie effective - basée sur la notion de réduction ... là on est proche des catégories)

  Persistance homologique

• Dynamique symbolique (SMACUB9L)

  Intervenant : Pierre Arnoux, Étienne Moutot

  L'objectif du cours est de présenter les bases de la dynamique symbolique, qui consiste à étudier les systèmes dynamiques en s'intéressant à leurs trajectoires dans une partition finie de l'espace. Le cours s'attardera en particulier sur des systèmes symboliques de dimension 2 et au delà, et leurs liens avec de nombreux résultats d'informatique théoriques (indécidabilité, algorithmes de fractions continues, ...).

  Plan du cours:

  Dynamique symbolique 1D (Étienne Moutot) :

  • Mots finis et infinis
  • Espaces de shift et entropie
  • Liens avec les systèmes dynamiques
  • Complexité et liens avec la périodicité

  Dynamique symbolique 2D (Étienne Moutot) :

  • Complexité de motifs en dimension supérieure
  • Conjecture de Nivat: exemples, contre-exemples et avancées récentes
  • (in)décidabilité de problèmes algorithmiques en dimensions supérieures

  Substitutions (Pierre Arnoux) :

  • Substitutions en dimension 1: Fibonacci et substitutions Sturmiennes
  • Liens avec la complexité
  • Substitutions en dimensions supérieures: Tribonacci, baderne de Rauzy
  • Liens avec les algorithmes de fractions continues et leurs généralisations
  • Codages de plans discrets

   

• Théorie de Ramsey (SMACUD8L)

  Intervenant : Lionel Nguyen Van Thé

  Théorème de Ramsey, fini et dénombrable.

  • Applications : Théorèmes d'Erdos-Szekeres sur les sous-suites monotones, et sur les polygones convexes du plan.
  • Bornes : Bornes sup et double récurrence, borne inf et méthode probabiliste.

  Théorèmes de partition en théorie des nombres :

  • Théorème de Schur.
  • Théorème de Rado sur les systèmes d'équations régulières par partitions.
  • Théorème de van der Waerden, via le théorème de Hales-Jewett.

  Théorie de Ramsey euclidienne :

  • Ensembles de Ramsey du plan: Tout ensemble de Ramsey est sphérique.
  • Nombre chromatique du plan. Prétexte de ce probème pour évoquer la pertinence de l'axiomatique de la théorie des ensembles.

  Théorie de Ramsey infinie : (le but de cette partie sera surtout de poursuivre la réflexion sur la pertinence de la théorie des ensembles en tant que cadre axiomatique)

  • Théorème de Hindman, via les ultrafiltres.
  • Théorème de Galvin-Prikry.
  • Le rôle de l'axiome du choix et des axiomes de détermination.

• Introduction aux systèmes dynamiques et à la théorie ergodique (SMACUD7L)

  Intervenants: Pierre Arnoux, Arnaud Hillion

  1. Théorie ergodique
     • Systèmes dynamiques mesurables. Exemples issus de la géométrie, de la dynamique symbolique et de la théorie des nombres.
     • Théorème de récurrence de Poincaré. Théorèmes ergodiques de von Neumann et de Birkhoff.
     • Propriétés ergodiques : ergodicité, mélange faible et théorie spectrale, mélange fort. Classification des systèmes à spectre discret. Entropie métrique.
  2. Dynamique topologique
     • Systèmes discrets (fonction) et systèmes continus (flots).
     • Systèmes dynamiques topologiques. Point fixe, périodique, récurrent. Ensemble errant et non-errant, transitivité topologique, mélange topologique, minimalité, entropie topologique. Exemples.
  3. Quelques constructions classiques
     • Application de premier retour d'un flot sur une section.
     • Suspension d'une application avec temps de retour donné.
     • Extension naturelle au sens de Rokhlin.
     • Construction de mesures invariantes.
     • Application à des problèmes de géométrie, de théorie des nombres et de combinatoire: du billard aux fractions continues, au flot géodésique sur la surface modulaire et aux substitutions.

• Combinatoire des mots (SMACUD4L)

  Intervenants : Julien Cassaigne

  Résumé ou plan du cours :

  • Combinatoire des mots finis (morphismes, codes, conjugaison, périodicité)
  • Combinatoire des mots infinis (mots morphiques, récurrence, complexité, graphes de Rauzy)
  • Quelques applications (en dynamique, en théorie des nombres)

  Théorie algorithmique des nombres (SMACUD5L)

  Intervenants : Yves Aubry, Stéphane Ballet, David Kohel, Stéphane Louboutin, Serge Vladut

  Résumé ou plan du cours:

  La théorie computationnelle des nombres suscite de plus en plus d’intérêt au sein de la société en raison de son utilité dans le domaine de la sécurité
  
  informatique en générale. L’utilisation d’algorithmes mettant en œuvre des objets mathématiques de plus en plus sophistiqués nécessite en amont une
  
  approche de la théorie algorithmique des nombres orienté vers l’effectivité. Dans ce cours, nous nous proposons donc d’étudier des algorithmes ou méthodes de calculs en géométrie algébrique effective :

  • algorithmique dans les corps finis
  • arithmétiques efficaces sur les courbes elliptiques
  • calculs explicites dans les espaces de Riemann-Roch définis sur des corps finis
  • arithmétique des algèbres de quaternions et courbes de Shimura
  • calculs explicites dans les corps de nombres

  Nous illustrerons le cours par des calculs en Sage et/ou Magma.

Algorithmique et combinatoire

• Fondements de la PPC et SAT (SMACUA7L)

  Intervenant : Philippe Jegou, Chu-Min Li

  Cette option traite des fondements de la programmation par contraintes (PPC) et de la résolution de SAT. Elle couvre les aspects allant des algorithmes, architectures et fondements théoriques des solveurs SAT et CSP, jusqu'à l'étude des classes polynomiales dans ces deux formalismes.

  Les points abordés portent sur :

  • classes polynomiales ("tractable classes") pour SAT, CSP et au-delà ;
    • classes définies par restrictions de langages,
    • classes définies par décomposition de graphes et hypergraphes (exploitation des résultats sur les problèmes exprimables en MSO sous l'hypothèse de largeurs bornées)
    • classe hybrides
  • architecture des solveurs :
    • algorithmes de résolution
    • algorithmes de propagation
    • heuristiques
    • clauses et no-goods learning
    • notion de redémarrage avec preuve de complétude
  • méthodes de résolution pour l'optimisation dans les formalismes VCSP, MaxSAT, WMaxSAT,
    • méthodes complètes (B&B et ses optimisations)
    • méthodes incomplètes (recherche locale, recherche tabou, algorithmes génétiques,...)
    • algorithmes de propagations de pondérations

• Algorithmique distribuée (SMACUA9L)

  Intervenants : J. Chalopin, S. Das, E. Godard, D. Imbs, A. Labourel

  L'objectif de ce cours est de présenter des problèmes fondamentaux d'algorithmique distribuée, ainsi que des résultats de calculabilité et de complexité associés. On utilisera des méthodes algorithmiques pour résoudre ces problèmes classiques et des méthodes combinatoires et topologiques pour montrer des résultats d'impossibilité et des bornes inférieures de complexité

  Modèlisation des Systèmes Distribués

  • Panorama des systèmes distribués
  • Calculabilité distribuée
  • Équivalence entre modèles
  • Vers un modèle unifié ?

  Systèmes à passages de messages

  • Modèles de communication
  • Algorithmes pour la diffusion et l'élection
  • Algorithmes probabilistes pour les réseaux anonymes

  Mémoire partagée

  • Impossibilité du consensus sans attente
  • Modèle du snapshot itéré et impossibilité du k-consensus
  • Diffusion tolérante aux défaillances
  • De la mémoire partagée aux réseaux dynamiques

  Agents mobiles

  • Modèles et mesures de complexité
  • Exploration et rendez-vous

  Selon les années et les intervenants, l'importance relative de ces différents thèmes pourra varier.

• Optimisation combinatoire (SMACUB4L)

  Intervenants : B. Couëtoux, G. Naves et Y. Vaxès

  Un problème d'optimisation combinatoire est caractérisé par un espace de solutions très grand mais que l'on peut décrire de manière compacte, comme l'ensemble des couplages, des st-chemins, des arbres couvrants ou des cycles hamiltoniens d'un graphe ou encore l'ensemble des permutations de n entiers. Une fonction objectif permet d'évaluer la qualité de chacune des solutions de l'espace de recherche. Résoudre un problème d'optimisation combinatoire c'est trouver une solution qui minimise ou maximise la fonction objectif. De nombreux problèmes aussi bien pratiques que théoriques se formulent de cette manière.

  L'objectif du cours est de présenter quelques idées fondamentales qui permettent de concevoir des algorithmes efficaces pour résoudre de façon exacte ou avec une garantie de performance des problèmes d'optimisation combinatoire.

  On insistera en particulier sur les notions suivantes :

  1. L'approche polyédrale consiste à représenter chaque solution de l'espace de recherche par son vecteur caractéristique et à étudier l'enveloppe convexe de ces vecteurs. Si celle-ci peut-être décrite de façon compacte (par exemple, par un nombre d'inégalités polynomial dans la taille de l'entrée du problème) alors la programmation linéaire permet d'obtenir un algorithme de résolution efficace.
  2. Une telle description vient souvent avec un résultat de type min-max qui permet de définir l'optimum du problème de minimisation que l'on cherche à résoudre comme l'optimum d'un autre problème de maximisation (ou l'inverse). La dualité de la programmation linéaire fournit un tel résultat. Elle est à la base de la conception de nombreux algorithmes efficaces (polynomial) de résolution exacte ou approchée via la méthode primale-duale.
  3. Même lorsqu'une représentation polyédrale compacte n'est pas disponible, en particulier pour les problèmes NP-difficiles, l'approximation de l'enveloppe convexe par des inégalités linéaires, appelées coupes, permet de fournir des bornes cruciales pour la résolution pratique des problèmes NP-difficiles par des méthodes de type séparation-évaluation-coupes (branch-and-cut). Nous illustrerons chacune de ces notions ou approches sur différents problèmes classiques : couplage, flot et coupes, arborescence, TSP, indépendant commun à deux matroïdes, arbre et réseau de Steiner, problème de localisation, etc.

  Selon les années et les intervenants, la liste des problèmes étudiés et l'importance relative des différentes notions pourra varier.

  Prérequis: Un intérêt pour les structures discrètes, la programmation linéaire et l'algorithmique. Toutes les notions utilisées dans le cours seront définies et expliquées.

• Théorie métrique des graphes (SMACUA8L)

  Intervenants : J. Chalopin, V. Chepoi et Y. Vaxès

  L'objectif du cours est de présenter les résultats principaux de la théorie métrique des graphes et des liens existant entre cette théorie et d'autres domaines comme la théorie géométrique des groupes ou la théorie de la concurrence.  On présentera des méthodes algorithmiques, combinatoires, géométriques et topologiques.

  Plongements isométriques dans des hypercubes et des produits de graphes

  Graphes médians, graphes bridged et la méthode "local vers global"

  • Équivalence entre les graphes médians, les complexes cubiques CAT(0) et les domaines de structures d'événements.
  • Équivalence entre graphes bridged et complexes simpliciaux systoliques

  Graphes et espaces hyperboliques au sens de Gromov

  • Métrique d'arbres et 0-hyperbolicité
  • Définitions et caractérisations de l'hyperbolicité
  • Propriétés algorithmiques des graphes hyperboliques
  • Problème du mot dans les groupes hyperboliques

  Plongement l_1 à faible distorsion et théorème de Bourgain. Applications algorithmiques

  Graphes de Helly et enveloppes injectives

  Selon les années et les intervenants, l'importance relative de ces différents thèmes pourra varier.

  Prérequis : Un intérêt pour la combinatoire, les structures discrètes et l'algorithmique. Toutes les notions utilisées dans le cours seront définies et expliquées.

• Ensembles ordonnés en combinatoire (SMACUB3L)

  Intervenants : F. Olive, F. Brucker, K. Knauer, L. Santocanale

  Résumé ou plan du cours :

  1. Ensembles ordonnées et treillis
  2. Largeur d'un ensemble ordonné et ses partitions en chaînes, théorème de  Dilworth.
  3. Ensembles ordonnés série parallèle (*)
  4. Familles d'ensembles fermés sous l'intersection (familles de Moore), opérateurs de clôture, connexions de Galois
  5. Treillis distributifs et modulaires
  6. Caractérisations locales des treillis (semi)distributifs et (semi)modulaires
  7. Bijection entre treillis distributifs et ensembles ordonnés finis, théorème de Birkhoff
  8. Treillis distributifs sur objets combinatoires: c-orientations des graphes, couplages des graphes bipartis planaires, tensions des graphes, pavages de dominos, treillis de chemins
  9. Matroïdes simples et treillis géométriques
  10. Géométries convexes, antimatroïdes, treillis semidistributifs
  11. Treillis semidistributifs sur objets combinatoires: arbres binaires,  (associaèdres, treillis de Tamari et Cambriens) ; permutations (permutoèdres)
  12. Groupes de Coxeter finis et leurs treillis (*)
  13. Hiérarchies (*)

  (*) : Selon le temps à disposition

Méthodes formelles

• Modélisation et simulation à événements discrets (SMACUB6L)

  Intervenants : L. Brenner, I. Demongodin, C. Frydman, A. Hamri

  Ce cours porte sur les méthodes de spécification des systèmes complexes et les formalismes à événements  discrets. Afin de maîtriser la spécification comportementale de ces systèmes, ce cours présente les formalismes permettant une spécification de haut niveau. Il fournit les bases théoriques en modélisation, analyse, simulation à événements discrets pour les domaines de l’informatique et des systèmes dynamiques complexes.

  Plan de cours :

  Présentation de divers formalismes à événements discrets avec et sans représentation du temps :

  • DEVS : Discrete EVent System Specification
  • RdP : Réseaux de Petri

• Théorie des automates : extensions et applications (SMACUB5L)

  Intervenants : N. Baudru, S. Fratani, B. Monmege, JM Talbot, PA Reynier

  L’objectif du cours est de présenter une ou plusieurs extensions du modèle classique des automates finis, en insistant sur les résultats positifs obtenus pour cette extension, les applications visées par cette extension, ainsi que les enjeux actuels.

  • Automates pondérés : équivalences entre automates et logiques, résultats de décidabilité, modèles pour les arbres et pour les mots, automates  probabilistes
  • Transducteurs : modèles unidirectionnels et bidirectionnels, modèle des SST, déterminisation et fonctionnalité
  • Ordre supérieur : langages indexés, langages d’ordre supérieur, automates à piles de piles

  Selon les années et les intervenants, la liste des problèmes étudiés et l'importance relative des différentes notions pourra varier.

  Prérequis: Un intérêt pour les automates, la logique et l’algorithmique. Toutes les notions utilisées dans le cours seront définies et expliquées.

• Vérification : de la théorie à la pratique (SMACUB1L)

  Intervenants potentiels : C. Bertolissi, D. Lugiez, R. Morin, JM Talbot, B. Monmege, PA Reynier

  Résumé ou plan du cours :

  L’objectif du cours est de montrer une ou plusieurs approches de type « méthode formelle » pour la vérification et/ou la synthèse. Il s’agira de présenter aux étudiants les bases théoriques sur lesquelles repose l’approche en question, et d’aller, dans la mesure du possible, jusqu’à la présentation d’outils logiciels existants.

  • Vérification et synthèse de systèmes temps-réel : automates et jeux temporisés, extensions à coûts et robustesse, logiciel UppAal TiGa
  • Vérification de protocoles cryptographiques : logique de séparation, logiciel ProVerif
  • Analyse et conception de systèmes distribués : théorie des traces de Mazurkiewicz, MSC, réseaux de Petri
  • Synthèse à partir de spécifications LTL : logique LTL, jeux de parité, extensions temps-réel
  • Sécurité de workflow : modélisation de politiques de sécurité et leurs propriétés, applications au contrôle d accès dans les processus métiers

  Selon les années et les intervenants, la liste des problèmes étudiés et l'importance relative des différentes notions pourra varier.

  Prérequis: Un intérêt pour les automates, la logique et l'algorithmique. Toutes les notions utilisées dans le cours seront définies et expliquées.

• Sémantique dénotationnelle et logique linéaire (SMACUB8L)

  Intervenants : Myriam Quatrini, Laurent Regnier, Lionel Vaux

  Dans une première partie le cours présente la sémantique dénotationnelle à partir de la notion d'espace cohérent, qui est à l'origine de la logique linéaire, dont on étudiera les propriétés. On présentera notamment le calcul des séquents de la logique linéaire, ainsi que la notion de réseau de preuve, qui fournit une approche asynchrone de l'élimination des coupures. On termine le cours par une ouverture à des sujets plus contemporains.

  Plan :

  1. Le modèle cohérent du λ-calcul.
  2. Logique linéaire : calcul des séquents et élimination des coupures.
  3. Réseaux de preuve et séquentialisation : le cas multiplicatif.
  4. Exponentielles dans les réseaux.
  5. Prolongements (au choix, en fonction du temps et des intervenants) :
     1. Au-delà du cas purement fonctionnel : opérateurs de contrôle ; concurrence.
     2. Sémantique quantitative et développement de Taylor.
     3. Focalisation et recherche de preuve.
     4. Ludique.

• Logique catégorique d'ordre supérieur (SMACUD2L)

  Intervenants : Dimitri Ara, Charles Grellois, Luigi Santocanale, Lionel Vaux

  Résumé ou plan du cours :

  Le cours se propose d'exposer certains développements de la logique contemporaine intégrant le langage des catégories comme un outil de description, de compréhension ou de conception. Historiquement motivée par la recherche fondamentale en logique et pour la conception des langages de programmation, cette approche est aujourd’hui vivante dans la pratique de la programmation fonctionnelle.

  Le cours sera éclairé par de nombreux exemples tirés des mathématiques (algèbre, ordres, topologie, etc.) et de l'informatique (automates, structures de données, programmation fonctionnelle, etc.).

  Progression :

  1.  Théorie des catégories
     1. Catégories, foncteurs, transformations naturelles
     2. Limites et colimites
     3. Adjonctions et monades
  2. Catégories cartésiennes fermées
     1. Catégories monoidales
     2. Catégories cartésiennes fermées et lambda-calcul simplement typé
     3. Modèles du lambda calcul pur (objets réflexifs) *
  3. Logique catégorique
     1. Logique intuitionniste d'ordre supérieur
     2. Théorie des ensembles intuitionniste *
     3. Modèles de réalisabilité
     4. Objet de valeur de vérité dans une catégorie et topos

  * : selon le temps à disposition.

• Réalisabilité classique (SMACUD3L)

  Intervenants : Étienne Miquey, Laurent Regnier, Lionel Vaux

  On commencera par rappeler les principes de la réalisabilité intuitionniste dans le cadre de l'arithmétique du second ordre, la présentation de la machine de Krivine pour le lambda-calcul avec continuations et son utilisation pour étendre la réalisabilité intuitionniste à la logique classique.

  On passera ensuite aux résultats de base de la théorie : réalisation du schéma de récurrence, terme de stockage, réalisation des formules du premier ordre de l'arithmétique.

  Si le temps le permet on abordera les extensions au cadre de la théorie des ensembles et l'on verra comment la réalisabilité peut être vue comme une extension du forcing permettant de construire des modèles inédits de ZFC.

• ASP : fondements théoriques, calculs et applications (SMACUB7L)

  Intervenants : Eric Würbel, Belaid Benhamou, Vincent Risch

  ASP est un paradigme de représentation et de raisonnement sur les connaissances, apparu il y a une vingtaine d'années, et qui connaît actuellement un développement important de par l'existence de solveurs efficaces. Le but de cette option est d'étudier ASP sous ses angles théoriques, calculatoires, et pratiques.

  • fondements théoriques :
    • modèles stables, non-monotonie
    • equilibrium logics, équivalences de programmes
    • sémantiques modales
  • calcul des modèles stables :
    • solveurs de type branch and bound
    • solveurs basés sur la recherche de conflits
  • applications :
    • ASP en pratique
    • méthodologies de développement

• Introduction à la logique modale (SMACUA5L)

  Intervenants : C. Greillois, E. Wurbel, V. Risch, N. Olivetti, L. Santocanale

  Résumé ou plan du cours :

  1. Introduction
  2. Sémantique de Kripke*
  3. Système fondamentaux : K, 4, 5, B, D, T,
  4. Axiomatisation et complétude des axiomatisations
  5. Systèmes de preuves et méthodes de décision (tableaux)
  6. Théorie de la correspondance (Salhqvist, Kracht) (*)
  7. Logique computationnelles (PDL, mu-calcul) (*)
  8. Logique modale pour l'lA (logique épistémique et autres) (*)

  (*) : selon le temps à disposition.