# Summer School in Logic in Computer Science''



+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Summer School announcement and latex file of the corresponding poster
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

First International Summer School in Logic for Computer Science

"PROOF THEORY and FOUNDATIONS OF PROGRAMMING"

June 28 -- July 9, 1993, University of Chambery (France)
Parc Scientifique Savoie-Technolac, Le Bourget-du-lac

The series of International Summer Schools in Logic for Computer
Science is part of the "Euroconferences" program of the European
Community, and is supported by the European Association for Computer
Science Logic.  It is intended primarily for young researchers in
Computer Science or in Mathematics, who are interested in "Logical
Tools and Methods for Computer Science", from the viewpoints of both
theory and applications.  Each school is devoted to a specific topic,
whose theoretical foundations have developed recently, and which has
promising applications.

The topic of this year's school is "Proof Theory and Foundations of
Programming". The lectures will analyse the relations between formal
proofs and programs, from their historical roots in Proof Theory and
Lambda Calculus to their most recent theoretical and practical
advances. The well-known correspondence between constructive proofs
and functional programs provides a theoretical framework for the
mathematization of programming, and has important consequences, which
include program correctness, modularity, and reusability.  The subject
is undergoing at present impressive developments in various
directions, including automatic extraction of programs from proofs,
correspondence between classical logic and imperative program
constructs, control of computational complexity at the level of proof
systems, and new computational paradigms derived from proof theory.

During the two week school participants would be able to attend
comprehensive courses as well as informal talks, and to take active
part in discussions of open problems.  The following courses will be
offered.

J.Y. GIRARD (Marseille, France):
Fundamentals of Proof Theory: Proofs and Types.

S. RONCHI (Torino, Italy):
Fundamentals of Lambda-calculus

S. BERARDI (Torino, Italy):
Program Extraction from Constructive Proofs

J.L. KRIVINE (Paris, France):
Programming with Proofs in Second Order Logic

D. LEIVANT (Bloomington, USA):
Computational Complexity inherent in Type Systems

M. PARIGOT (Paris, France):
Algorithmic Interpretations of Classical Logic

L. REGNIER (Marseille, France):
New Models of Execution derived from Proof Nets

A. SCEDROV (Philadelphia, USA):
Linear Logic

J. TIURYN (Warsaw, Poland):
Type Reconstruction

The school will take place at the University of Chambery, near Lake
Bourget (Lac du Bourget'') in the High Alps.  In addition to its
stunning alpine setting, Chambery offers a broad range of activities
and recreations, benefitting from its proximity to both high mountains
and an 18 km long lake.  Participants will also be offered organized
activities.

The participation fees amount to 5200 FF, which include registration
fees and living expenses (lodging, meals, coffee breaks, ...etc).
A limited number of grants will be offered.

Deadline for Applications: April 15th 1993

For further information and application forms for participation and
M. Parigot / School LCS, Laboratoire de Logique, UFR de Math\'ematiques,
Universit\'e Paris 7, 2 place Jussieu, 75251 Paris Cedex 05, France
e-mail: school@logique.jussieu.fr

School Director: M. Parigot
Organizing Committee: R. David, N. Bernard, J. Doyen

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Here is the latex file of a poster of the School "PROOF THEORY and
FOUNDATIONS OF PROGRAMMING", that can be printed and stuck. A big
and colour poster is a also available on request at school@logique.jussieu.fr
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

\documentstyle{report}

\textwidth 17.8cm
\textheight 26cm
\topmargin -2cm
\oddsidemargin -1cm
\evensidemargin -1cm
\pagestyle{empty}
\begin{document}

\begin{center}
{\Large {\bf First International Summer School in Logic for Computer Science}}
\end{center}

\vspace{3 mm}
\begin{center}
{\Huge { PROOF THEORY}}\\
\vspace{2 mm}
\hspace{-5 mm}{\Large {\bf \&}}\\
\vspace{3.5 mm}
{\Huge { FOUNDATIONS OF PROGRAMMING}}
\end{center}

\vspace{3 mm}

\begin{center}
{\Large June 28 -- July 9, 1993, University of Chamb\'ery (France)}\\
\vspace{1.5 mm}
{\large Parc Scientifique Savoie-Technolac, Le Bourget-du-lac}
\end{center}

\vspace{7 mm}

\noindent
The series of International Summer Schools in Logic for Computer Science
is part of the {\it Euroconferences} program of the European Community,
and is supported by the European Association for Computer Science Logic.
It is intended primarily for young researchers in Computer Science or
in Mathematics, who are interested in {\it Logical Tools and Methods
for Computer Science}, from the viewpoints of both theory and applications.
Each school is devoted to a specific topic, whose theoretical foundations
have developed recently, and which has promising applications.

\medskip \

\noindent
\begin{minipage}[t]{8.4cm}
\begin{center}
{ {\bf J.Y. GIRARD}, { Marseille, France}\\
{\it Fundamentals of Proof Theory: Proofs and Types}}\\
\medskip
{ {\bf S. RONCHI}, { Torino, Italy} \\
{\it Fundamentals of $\lambda$-calculus}}\\
\medskip
{ {\bf S. BERARDI}, { Torino, Italy} \\
{\it Program Extraction from Constructive Proofs}}\\
\medskip
{ {\bf J.L. KRIVINE}, { Paris, France} \\
{\it  Programming with Proofs in Second Order Logic}}\\
\medskip
{ {\bf D. LEIVANT}, { Bloomington, USA} \\
{\it Computational Complexity inherent in Type Systems}}\\
\medskip
{ {\bf M. PARIGOT}, { Paris, France}\\
{\it Algorithmic Interpretations of Classical Logic}} \\
\medskip
{ {\bf L. REGNIER}, { Marseille, France}\\
{\it New Models of Execution derived from Proof Nets}} \\
\medskip
{ {\bf A. SCEDROV}, { Philadelphia, USA}\\
{\it Linear Logic}}\\
\medskip
{ {\bf J. TIURYN}, { Warsaw, Poland}\\
{\it Type Reconstruction}}\\
\end{center}
\end{minipage}\
\hspace{1.3cm}
\begin{minipage}[t]{7.9cm}

The topic of this year's school is {\it Proof Theory and Foundations of
Programming}. The lectures will analyse the relations between formal
proofs and programs, from their historical roots in Proof Theory and
Lambda Calculus to their most recent theoretical and practical
advances. The well-known correspondence between constructive proofs and
functional programs provides a theoretical framework for the
mathematization of programming, and has important consequences,
which include program correctness, modularity, and reusability.
The subject is undergoing at present impressive developments
in various directions,  including
automatic extraction of programs from proofs,
correspondence between classical
logic and imperative program constructs, control of computational
complexity at the level of proof systems, and new computational
paradigms derived from proof theory.

During the two week school participants would be able to attend
comprehensive courses, whose list is indicated, as well as informal talks,
and to take active part in discussions of open problems.

\end{minipage}

\bigskip \

\noindent
The school will take place at the University of
Chamb\'ery, near Lake Bourget (Lac du Bourget'') in the High Alps.
In addition to its stunning alpine setting, Chamb\'ery offers a broad
range of activities and recreations, benefitting from its proximity to
both high mountains and an 18 km long lake.  Participants will also be offered
organized activities.

\noindent
A limited number of {\it grants} will be offered,
covering living expenses and registration fees.

\medskip

\begin{center}
\noindent
{\bf Deadline for Applications: April 15th 1993}

\medskip
\noindent
For further information and application forms for participation and for grants
M. Parigot / School LCS, Laboratoire de Logique, UFR de Math\'ematiques, \\
Universit\'e Paris 7, 2 place Jussieu, 75251 Paris Cedex 05, France \\
e-mail: {\tt school@logique.jussieu.fr}
\end{center}

\bigskip

\noindent
{\large {\bf School Director}: M. Parigot \hfill\
{\bf Organizing Committee}: R. David, N. Bernard, J. Doyen}

\end{document}