Difference between revisions of "Courses/LOFO"
From LRDE
Line 10: | Line 10: | ||
|optional course=oui |
|optional course=oui |
||
|module=Sciences Générales |
|module=Sciences Générales |
||
+ | |prerequisites=* Capacité à comprendre et écrire des preuves par récurrence. * Capacité à lire des formules mathématiques et à exprimer des propriétés sous forme de formule.Il est souhaitable mais pas obligatoire d'avoir suivi LOGI. |
||
− | |prerequisites=Programme Classes Préparatoires, LOGI |
||
+ | |objectives=Ce cours présente principalement deux notions théoriques avec des applications concrètes en informatique : |
||
− | |objectives=Le véritable but de ce cours est de présenter l’isomorphisme de Curry-Howard, qui montre une correspondance profonde, et surprenante, entre le programmes et démonstrations. À cette fin tous les prérequis sont introduits dans un premier temps. Ils sont intéressants en soi pour la culture de l’informaticien sensible aux aspects formels. |
||
+ | * Les systèmes de preuves, qui introduisent la notion de vérité comme construction obtenue à partir d'une série de déductions ; des logiciels de preuve comme COQ ou des langages certifiés comme l'Atelier B en dépendent. |
||
+ | * Le lambda calcul, formalisme de programmation différent des machines de Turing mais tout aussi puissant, qui sert de base à la programmation fonctionnelle. |
||
+ | Ces deux notions sont reliées par l'isomorphisme de Curry-Howard. Un programme est donc d'une certaine manière une forme de preuve mathématique. |
||
|content=# Lambda calcul |
|content=# Lambda calcul |
||
# Lambda calcul simplement typé |
# Lambda calcul simplement typé |
Revision as of 14:18, 3 July 2020
Titre |
Logique formelle |
---|---|
Sigle |
LOFO |
Enseignant | |
Période |
S4, Ing1 |
Public |
Tronc-commun |
Contrôle |
Partiel |
Durée |
12h |
Optionnel |
oui |
Module |
Sciences Générales |
Prérequis |
|
Objectifs |
Ce cours présente principalement deux notions théoriques avec des applications concrètes en informatique :
Ces deux notions sont reliées par l'isomorphisme de Curry-Howard. Un programme est donc d'une certaine manière une forme de preuve mathématique. |
Plan |
|
Documentation | |
Support | |
Journaux |