# School announcement


PRELIMINARY ANNOUNCEMENT

ADVANCED SCHOOL ON TYPED LAMBDA CALCULUS AND FUNCTIONAL PROGRAMMING

September 19 - September 30, 1994
CISM, Palazzo del Torso,
Piazza Garibaldi, 18 - UDINE Udine (ITALY)

The Advanced School is organized under the auspices of the Italian
Chapter of EATCS (European Association for Theoretical Computer
Science) and UNESCO.  It is supported also by the University of Udine
and the CNR.

Formal Methods for specifying, modularizing, verifying, and reusing
large programs and systems, as well as principled languages, which
allow to apply rapidly such methods, are greatly needed in Computer
Science.

Typed Lambda Calculus has been recently understood as a central node
in a conceptual network which links various fields of Logic to
Computer Science.  It has made possible to transfer fruitfully ideas
and techniques from Category Theory, Proof Theory, Type Theory to
Computer Science. Based on formally solid and conceptually disciplined
logical grounds, Typed Lambda Calculus allows for the development of a
mathematically clear style of programming as well as for the design of
flexible logical tools and methods for Computer Science.

In recent years, Typed Lambda Calculus has been impressively used also
as a metalanguage for defining formal systems for reasoning about
Programs and as a logical framework for designing interactive proof
assistants} for computer aided formal reasoning.

The School will offer 5 series of (approx.8-10) introductory and
advanced lectures on the connections between Typed Lambda Calculus and
Category Theory, Proof Theory, and Type Theory, and on the, more
recent, applications of Typed Lambda Calculus, such as the design of
Typed Functional Languages, General Proof Assistants, and Program
Logics.

SCHOOL DIRECTORS

M. DEZANI CIANCAGLINI (Torino)
FURIO HONSELL (Udine)

LIST OF SPEAKERS

JEAN-YVES GIRARD  (Marseilles)
Proof Theoretic Foundations

GERARD HUET  (INRIA Rocquencourt)
Advanced Typed Functional Languages: Theorem Proving in Coq

JOHN MITCHELL  (Stanford)
Programming Languages and Types

EUGENIO MOGGI (Genova)
Meta-languages and Applications

S. RONCHI DELLA ROCCA  (Torino)
Basic Lambda Calculus

The School is intended primarily for young researchers and PhD
students in Computer Science and Mathematics. During the School,
participants will be able to attend also informal talks and
discussions of open problems.  PhD students may ask to sit for an
examination at the School. It will consist of a Seminar on a topic
agreed upon by the Directors and the Speakers.  There will be
demonstrations, and participants will have the opportunity to use a
computer environment.

To apply, participants should fill the form (to be publicized shortly)
and return it together with a recommandation letter to:

Professor F.Honsell
Universita' di Udine,
Dipartimento di Matematica e Informatica
via Zanon, 6,
33100 UDINE - ITALY
Tel: 39-432-272220  Fax:  39-432-510755

The DEADLINE for application is July 31st 1994. Further information can
be obtained via email under the address:

scuola@dimi.uniud.it

FEES and SCHOLARSHIPS
The participation fee is 650.000 Italian Liras.
There is a limited number of scholarships available for people who
cannot obtain funding for their travel, participation fee and living
expenses from their institutions. A request for full or partial
support should be enclosed with the applications.

-----------LateX file------------------
\documentstyle{article}

\parindent 0cm
\pagestyle{empty}
\textwidth 18 cm
\textheight 28cm
\topmargin -2.5cm
\oddsidemargin -1.2cm
\evensidemargin -1.2cm
\begin{document}
\begin{minipage}[t]{18cm}
\begin{center}
{\LARGE Preliminary Announcement} \end{center}
\smallskip

\begin{center}
{\Huge Advanced School on Typed Lambda Calculus
} \end{center}
\begin{center}
{\Huge and Functional Programming} \end{center}

\begin{center}
{\LARGE September 19 - September 30, 1994}\\ {\Large CISM, Palazzo del Torso,
Piazza Garibaldi, 18 - UDINE Udine (ITALY)} \end{center} \bigskip
\end{minipage}
The Advanced School is organized under the auspices of the Italian Chapter of
EATCS (European Association for Theoretical Computer Science) and UNESCO.
It is supported also by the University of Udine and the CNR.

\bigskip
\begin{minipage}[t]{ 10 cm}
{\em
Formal Methods} for {\em specifying, modularizing, verifying, and reusing}
large programs and systems, as well as {\em principled languages}, which
allow to apply rapidly such methods, are greatly needed in Computer Science.

{\em Typed Lambda Calculus} has been recently understood as a central
node
in a conceptual network  which links various fields of {\em Logic}
to {\em Computer Science}.
It has
made possible to transfer fruitfully ideas and techniques from {\em
Category Theory}, {\em Proof Theory}, and {\em Type Theory} to Computer
Science.
Based on formally
solid and conceptually disciplined logical grounds, Typed Lambda Calculus
allows for the development of a mathematically clear style of programming
as well as for the design of flexible logical tools and methods for Computer
Science. In recent years, Typed Lambda Calculus has been impressively used
also as a {\em metalanguage} for defining formal systems for {\em reasoning}
about programs and as a {\em logical framework} for designing {\em interactive
proof assistants} for computer aided formal reasoning.

The School
will offer 5 series of (approx.8-10) introductory and advanced lectures
on the connections between Typed Lambda Calculus and
Category
Theory, Proof Theory, and Type Theory, and on the, more recent, applications of
Typed Lambda Calculus, such as the design of Typed Functional Languages,
General Proof Assistants, and Program Logics.
\end{minipage}
\ \
\begin{minipage}[t] {7cm}
\begin{center}
\smallskip
{\Large {\bf School Directors}}
\smallskip \\
{\bf  M. DEZANI CIANCAGLINI} (Torino)\\
{\bf FURIO HONSELL} (Udine)\\
\smallskip
\end{center}
\begin{center}
{\Large {\bf List of Speakers}}\\
\end{center}
\begin{center}
{\bf JEAN-YVES GIRARD}%(Marseilles) \\
{\em Proof Theoretic Foundations}  \end{center}
\begin{center}
{\bf GERARD HUET}%(INRIA Rocquencourt)  \\
Theorem Proving in Coq}\end{center}
\begin{center}
{\bf JOHN MITCHELL}%(Stanford) \\
{\em Programming Languages and Types}
\end{center}
\begin{center}
{\bf EUGENIO MOGGI}%(Genova) \\
{\em Meta-languages and Applications}
\end{center}
\begin{center}
{\bf S. RONCHI DELLA ROCCA}%(Torino)  \\
{\em Basic Lambda Calculus}
\end{center}
\end{minipage}
\bigskip

The School is intended primarily for young researchers and PhD students in
Computer Science and Mathematics. During the School, participants will be able
to attend also informal talks and discussions of open problems.
PhD students may ask to sit for an examination at the School. It will consist
of a Seminar on a topic agreed upon by the Directors and the Speakers.
There will be demonstrations, and
participants will have the opportunity to use a computer environment.

\bigskip
To apply, participants should fill the form (to be publicized shortly) and
return it together with a recommandation letter to:
\begin{center}
Professor F.%Honsell \\
Universit\{a} di Udine,
Dipartimento di Matematica e Informatica \\
via Zanon, 6,
33100 UDINE -
ITALY\\
Tel: 39-432-272220%%Fax:  39-432-510755 \end{center}

The {\bf DEADLINE} for application is July 31st 1994. Further informations can
be obtained via email under the address:
\begin{center} {\tt scuola@dimi.uniud.it} \end{center}

{\Large {\bf Fees and Scholarships}}
\smallskip \\
The participation fee is 650.000 Italian Liras.
There is a limited number of scholarships available for people who cannot
obtain funding for their travel, participation fee and living expenses from
their institutions. A request for full or partial support should be enclosed
with the applications.  \bigskip
\end{document}

-------text file---------------
`