40 HEE, 24 HPE

Code : 3IF221

Contact

Benoît Valiron benoit.valiron@centralesupelec.fr

Prérequis

Cursus commun en informatique

Présentation générale

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.

Acquis d’apprentissage visés dans le cours :

À l'issu de ce cours, les étudiants seront capables de :

• Modéliser un problème dans un cadre fonctionnel
• Connaitre 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

Moyens

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.

Description des compétences acquises à l'issue du cours

Compétence C2.1 - Avoir approfondi un domaine ou une discipline relatifs aux sciences fondamentales ou aux sciences de l'ingénieur

Compétence C6.4 - Résoudre des problèmes dans une démarche de pensée computationnelle

Contenu

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

Méthodes pédagogiques

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.

Méthodes d'évaluation

L'évaluation consiste en du contrôle continu et un projet noté.