Logique et systèmes déductifs
Ref: 3IF2211
Description
- Dans ce cours, nous brosserons à grands traits un aspect théorique important pour les sciences du logiciel: la modélisation dans un cadre fonctionnel. Nous étudierons d'une part des modèles de calcul basé sur la réécriture c'est à dire un cadre général d'évaluation d'un algorithme ou d'un programme donné. Un focus particulier sera mis sur le lambda-calcul. D'autre part, nous passerons en revue trois systèmes logiques permettant de formaliser des théories et propositions logiques: Les types dépendants, HOL et la logique de Hoare. Le lien entre les deux sera présenté sous l'angle des systèmes de types.
Période(s) du cours
SM10
Prérequis
- Cursus commun en informatique
Syllabus
Calcul
- Universalité, thèse de Church Turing, Calculabilité, Problème de l'arrêt
- Réécriture de 1er ordre, Lambda-calcul, stratégie de réduction
- Systèmes de type, types récursifs, types dépendants
- Inférence de type et compilation
Logique
- 1er et 2nd ordre, logique intuitioniste et logique classique
- Équivalence de Curry-Howard
- Expressivité, décidabilité (ZFC, Presburger, etc)
- SAT/SMT
Systèmes déductifs
- Forme de preuve
- Raisonnement inductif
- Types dépendants, HOL, logique de Hoare
Composition du cours
Le cours module théorie et application, la théorie servant de fil
directeur pour une compréhension fine des processus en jeu dans les
outils et méthodes présentés en TD.
Ressources
Le cours se compose de 3 parties, chacune couvrant en moyenne 5 séances
de 1h30 (typiquement 3 séances de cours et 2 TDs/TPs). La coloration et
le poids des différentes parties peuvent évoluer en fonction des
besoins.
Résultats de l'apprentissage couverts par le cours
À l'issu de ce cours, les étudiants seront capables de :
- Modéliser un problème dans un cadre fonctionnel
- Connaître les grandes classes de systèmes logiques et leur relations
- Caractériser la correspondance entre un système logique et un modèle de calcul à travers Curry-Howard
Support de cours, bibliographie
- Pierce, B. C. (2002). Types and programming languages. MIT press.
- Appel, A. W. (2007). Compiling with continuations. Cambridge university press.
- Bertot, Y., & Castéran, P. (2015). Le coq’art (v8).
- Nipkow, T., & Klein, G. (2014). Concrete semantics: with Isabelle/HOL. Springer International Publishing.