Difference between revisions of "Courses/LOFO"
From LRDE
Line 2: | Line 2: | ||
|title=Logique formelle |
|title=Logique formelle |
||
|acronym=LOFO |
|acronym=LOFO |
||
− | |teacher=Max |
+ | |teacher=Max |
|period=S4, Ing1 |
|period=S4, Ing1 |
||
|audience=Tronc-commun |
|audience=Tronc-commun |
||
Line 9: | Line 9: | ||
|optional course=oui |
|optional course=oui |
||
|module=Sciences Générales |
|module=Sciences Générales |
||
− | |prerequisites=Programme Classes Préparatoires |
+ | |prerequisites=Programme Classes Préparatoires, LOGI |
|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. |
|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. |
||
|content=1) Lambda calcul |
|content=1) Lambda calcul |
Revision as of 09:33, 21 March 2017
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 |
Programme Classes Préparatoires, LOGI |
Objectifs |
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. |
Plan |
1) Lambda calcul 2) Lambda calcul simplement typé 3) Déduction naturelle pour la logique classique 4) Calcul des séquents, élimination des coupures 5) TD Lambda Calcul / Systèmes de déduction 6) Logique Intuitionniste 7) Isomorphisme de Curry-Howard
|
Documentation | |
Support | |
Journaux |