Master 2 - Programmation et Logiciel Sure
Programmes et Preuves
2009/2010
Stefano Guerrini
- Calendrier
- Support du cours
Calendrier
- 08/01/2009:
13h45-17h00 - C211
Rappelle de notions de base
- Rappelles sur la validité des formules du calcul propositionnelle.
- Le calcul des séquents pour la logique classique (LK):
séquents dérivables et correction par rapport à la validité logique.
Support du cours:
- 15/01/2009:
13h45-17h00 - C212
Élimination des coupures.
- Théorème d'élimination des coupures.
- Règles d'élimination des coupures pour les cas principales.
- Le cross-cut.
Support du cours:
TD:
- 22/01/2009:
13h45-17h00 - B107
-- Annulé --
- 29/01/2009:
13h45-17h00 - B107
Démonstration du lemme principal de l'élimination des coupures
(lemme du cross-cut)
Support du cours:
TD:
- 03/02/2009:
13h45-17h00 - Amphi A
Rattrapage du cours annulé le 22/01
TD
- 05/02/2009:
13h45-17h00 - B107
Rappel sur la déduction à la Hilbert (axiomes, modus ponens)
La déduction naturelle.
Support du cours:
TD
- 12/03/2009:
13h45-15h15 - B107
La déduction naturelle.
Support du cours:
- 19/03/2009:
13h45-17h00 - B107
$\lambda$-calcul et déduction naturelle.
Correspondance Curry-Howard.
Logique intuitionniste.
Support du cours:
TD
- 26/03/2009:
14h00-17h00 - F003
Partiel - Durée prevu entre 2h30 et 3h00
Les exercices du partiel sur la partie de logique porterons sur les arguments presentés dans les cours et exemplifiés dans la feuille de exercices td4 (corrigés). Notamment:
- Calcul des séquents de la logique classique
- Élimination des coupures
- Déduction naturelle
- Correspondance Curry-Howard entre preuves de la déduction naturelle et termed du λ-calcul
- Déduction naturelle et calcul des séquents pour la logique intuitionniste
NB Par rapport à la feuille TD4, dans le partiel il y aura plus d'exercices mais plus simples et avec des réponses plus courtes.
Support du cours
Proofs and Types
stefano.guerrini@univ-paris13.fr
Last modified: Sat Mar 27 22:17:59 CET 2010