Cours commun Ulm-Cachan “Logique et Informatique”

		Cours
Où?	Where?	ENS Cachan (plan d'accès) bât. Cournot, salle 311 (3ème étage)
Quand?	When?	Le mardi de 14h00 à 18h15
Par qui?	Who?	Jean Goubault-Larrecq
		Etienne Lozes

Le cours est en trois parties:

Lambda-calcul pur, (non-)terminaison, confluence, standardisation. Le poly, aussi en format html.
Lambda-calcul typé, correspondances de Curry-Howard pour diverses logiques, classiques ou intuitionnistes, allant de la logique propositionnelle minimale (types simples) à l'arithmétique du second ordre (système F). Le poly, aussi en format html.
Machines, lambda-calculs à substitutions explicites, et propriétés mathématiques d'iceux. Le poly, aussi en format html.

Examens des années précédentes:

(2000) Relations logiques et théorème de Friedman, énoncé et correction;
(2001) Lambda-upsilon calcul, types intersection et préservation de la normalisation forte, énoncé et correction.
(2002) Le lambda-calcul monadique (ou méta-langage de Moggi), énoncé et correction.
(2003) Lambda-upsilon calcul (le retour!), confluence et machines, énoncé et correction.
(2004) Réductions closes, énoncé et correction.
(2005) Systèmes de types intersection et modèles de filtres, énoncé et correction.
(2006) Propriétés de normalisation du λσ-calcul, énoncé et correction.
(2007) Types récursifs, énoncé et correction.
(2008, devoir) Logique modale intuitionniste S4, énoncé et correction.
(2008, examen) Système F_ω, logique d'ordre supérieur, énoncé et correction.
(2009, devoir) Le λ-calcul avec paires surjectives, énoncé et correction.
(2009, examen) Le λ-calcul étiqueté, énoncé et correction.
(2011, devoir) Adéquation en PCF, énoncé et correction.

This document was translated from L^AT_EX by H^EV^EA.