Descriptif
La logique informatique est utilisé dans un large éventail d'applications en informatique, allant de l'approche déductive de l'Intelligence Artificielle préconisée par le pionnier de l'IA, John McCarthy, à la démonstration de l'absence de bogues dans de grands logiciels industriels, comme la ligne 14 du métro de Paris, ou à vérifier les théorèmes difficiles comme celui de Feit-Thompson dans la classification des groupes simples finis. L'objectif de ce cours est d'expliquer la manière dont la logique peut être utilisée afin de modéliser des problèmes de nature informatique ou mathématique, et comment les ordinateurs peuvent être utilisés pour y parvenir. Nous allons présenter des assistants de preuve, qui permettent de formaliser un raisonnement humain par la construction interactive de preuves, et expliquent leur utilité pour certifier l'absence de bogues dans les programmes. Il est basé sur la correspondance Curry-Howard : un programme est identique à une preuve (ou plus précisemment, un programme fonctionnel typé correspond à une dérivation de son type). Afin d'atteindre des applications réalistes, nous présenterons l'assistant de preuve Agda et la logique dépendente qu'il sous tend. Si le temps nous le permet, nous présenterons également différentes notions et techniques telles que la théorie des ensembles et la recherche de preuve. Ce cours est aussi à propos de logique en pratique : toutes les PC se feront sur ordinateurs, utilisant OCaml puis Agda. Site du cours :Objectifs pédagogiques
Les objectifs du cours sont d'acquérir - les bases en programmation fonctionnelle : notions fondamentales (fonctions, lieurs, réduction), formalisation (λ-calcul), propriétés (confluence), expressivité (complétude au sens de Turing), implémentation - les bases des systèmes de types : fonctionnement (règles, inférence), garanties apportées (réduction du sujet, progrès, terminaison), variantes (types dépendants) - une connaissance de la logique : propriétés fondamentales (cohérence, élimination des coupures), systèmes (calcul des prédicats, premier ordre, types dépendants), constructivité (logique intuitionniste ou classique), formalismes (déduction naturelle, séquents) - la correspondance preuve-programme : λ-calcul simplement typé et extensions (divers connecteurs, types dépendants), utilisation pour les assistants de preuve - les bases de l'assistant de preuve Agda : utilisation, types inductifs, techniques de preuve, traitement de l'égalité
36 heures en présentiel
Diplôme(s) concerné(s)
- M1 MPRI - Fondements de l'Informatique
- M1 CPS - Système Cyber Physique
- M2 CPS - Système Cyber Physique
- M2 CSN - Computer Science for Networks
- M1 DATAAI - Data and Artificial Intelligence
