Cours commun Ulm-Cachan “Logique et Informatique”

		Cours
Où?	Where?	ENS Paris-Saclay (plan d’accès) bât. Cournot, salle 315 (3ème étage)
Quand?	When?	Le mardi de 14h à 18h
Par qui?	Who?	Jean Goubault-Larrecq
		Stéphane Le Roux

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.

Quelques examens des années précédentes:

(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.
(2014, examen) Types de données en système F, énoncé et correction.
(2017, devoir) Quelques modèles de graphes du λ-calcul, énoncé et correction.
(2019, devoir) Le λ-calcul algébrique; réductions de tête et types intersection, énoncé et correction.
(2019, examen) Un cas particulier terminant du λ-calcul algébrique; le λυ-calcul, énoncé et correction.

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