[Prev][Next][Index][Thread]
CRIM Intensive Course
The following is an announcement of an intensive course
on lambda calculus, type theory, and linear logic
(taught mostly in French) to be held February 1-5 1993.
If you are interested, please contact Pr. G. Blanc,
Mathematiques, Faculte des Sciences de Luminy, 163
Avenue de Luminy, 13288 MARSEILLE Cedex O9,
email : gblanc@lumimaths.univ-mrs.fr
\documentstyle[11pt]{article}
\begin{document}
\begin{center}
COURS de DEA INTENSIF au CIRM
lambda-calcul typ\'e et logique lin\'eaire
1-5 f\'evrier 1993
\end{center}
Le cours fait partie du DEA de math\'ematiques de Marseille ainsi que
du DEA de maths-info; il fait partie de l'unit\'e ``logique et
programmation{''} dont l'autre cours ``programmation par
contraintes{''} est assur\'e par Georges Blanc. Ce cours intensif,
centr\'e sur une semaine, est ouvert aux \'etudiants d'autres DEA
interess\'es par le lambda-calcul type. La DRED finance des s\'ejours
et des voyages pour une quinzaine d'\'etudiants, qui seront
s\'electionn\'es sur dossier; il est bien entendu possible de
participer au DEA en payant la pension CIRM. Les \'etudiants
\'etrangers, en particulier europ\'eens, sont les bienvenus, \`a
condition qu'ils puissent suivre des cours pour l'essentiel en fran\c
cais. Le sujet du lambda-calcul typ\'e prend sa source dans le
constructivisme et la th\'eorie de la d\'emonstration; mais c'est avec
l'informatique que ce domaine prend sa v\'eritable dimension
d'approche \`a la programmation. L'\'equipe de logique du Laboratoire
de Math\'ematiques Discr\`etes de Luminy a centr\'e son activit\'e sur
le lambda-calcul typ\'e. La logique lin\'eaire est, \`a l'int\'erieur
de ce th\`eme un d\'eveloppement porteur de nouvelles potentialit\'es.
Un cours ``classique{''} de 5 fois 3 heures sur le lambda-calcul
typ\'e sera assur\'e par Jean-Yves Girard et suivra dans les grandes
lignes son livre~: ``proofs and types{''} (Cambridge tracts in
theoretical computer science, 1989).
Ce cours sera relay\'e par quatre cours plus avanc\'es sur des
domaines en prise sur la recherche~; les enseignants en sont choisis
parmi les meilleurs jeunes chercheurs; \`a noter la pr\'esence d'un
am\'ericain qui ne parle pas fran\c{c}ais, et donc d'un cours en
anglais. La dur\'ee des cours est de 3 heures chacun.
Le programme est approximativement le suivant~:
\begin{list}{}{\setlength{\itemsep}{0pt}}
\item {\bf Lundi matin}~: J-Y G : s\'equents, d\'eduction naturelle,
lambda-calculs.
\item {\bf Lundi apr\`es-midi}~: J-Y G : syst\`eme {\bf F},
th\'eor\`emes principaux.
\item {\bf Mardi matin}~: J-Y G : s\'emantique d\'enotationnelle.
\item {\bf Mardi apr\`es-midi}~: Thomas Ehrhard (LITP, Paris 7):
la s\'equentialit\'e.
\item {\bf Mercredi matin}::J-Y G : \'el\'ements de logique lin\'eaire
\item {\bf Mercredi apr\`es-midi}~: d\'etente
\item {\bf Jeudi matin}~: Patrick Lincoln (Stanford)~: decision problems in
Linear Logic
\item {\bf Jeudi apr\`es-midi}~: J-Y G ~: r\'eseaux de d\'emonstration
\item {\bf Vendredi matin}~: Yves Lafont (CNRS, Maths Discr\`etes)~:
r\'eseaux d'interaction
\item {\bf Vendredi apr\`es-midi}~: Vincent Danos (CNRS, Logique Paris 7)~:
g\'eom\'etrie de l'interaction
\end{list}
\dots\ les organisateurs se r\'eservant le droit de modification de ce
programme sans pr\'eavis.
Please Contact Pr. G. Blanc, Mathematiques, Faculte des Sciences de Luminy, 163
Avenue de Luminy, 13288 MARSEILLE Cedex O9,
email : gblanc@lumimaths.univ-mrs.fr
\end{document}