[Prev][Next][Index][Thread]
Summer School on SEMANTICS AND LOGICS OF COMPUTATION
A Newton Institute Summer School
SEMANTICS AND LOGICS OF COMPUTATION
25--29 September 1995
Newton Institute, Cambridge, UK
in collaboration with the
ESPRIT CLICS-II project
Second Call for Registration
The Summer School on Semantics and Logics of Computation is being held
as part of a six-month research programme on Semantics of Computation
at the Isaac Newton Institute for Mathematical Sciences, a new
international research centre in Cambridge UK. The Summer School is
sponsored by the CEC ESPRIT research project "Categorical Logic in
Computer Science, II" (CLICS-II). The aim is to present a number of
modern developments in semantics and logics of computation in a way
that is accessible to graduate-level students. Registrations from
postgraduate students will be given priority, but applications by
interested academics and industrialists are also welcomed.
===============================COURSES================================
Samson Abramsky (Imperial)
"Semantics of interaction"
(4 lectures)
course content t.b.a.
----------------------------------------------------------------------
Thierry Coquand (Chalmers)
"Computational content of classical logic"
(4 lectures)
I will give an introduction to the problem of extracting constructive
content from classical proofs. This problem has an interesting
history since it was an important part of Hilbert's program, who
wanted to "secure" non-constructive parts of mathematics. It has been
revived recently by the discovery of intringuing connections with some
concepts in computer science through the work of (among others)
C. Murthy, M. Parigot (lambda-mu calculus), J.L. Krivine (connection
with imperative programing), Ph. de Groote (connections with
exceptions in ML), and S. Berardi (symmetric lambda-calculus). I will
try to provide both historical and mathematical background to this
problem and to present concrete examples of non-constructive reasoning
in mathematics that is constructively problematic. The emphasis will
be on the proof-theoretical side, but I hope that this course will
motivate and serve as an introduction to the more recent, computer
science oriented work cited above (which will be described briefly).
A tentative plan is the following
Lecture 1: negative (double negation) translation, Friedman's
A-translation. An existential statement provable in PA is provable in
HA.
Lecture 2: Gentzen's sequent calculus, first consistency proof for
classical arithmetic. Connection to Novikov's calculus and
game-theoretic interpretation.
Lecture 3: problem with the combination Axiom of Choice + Excluded
Middle. How this problem is solved in C. Murthy's thesis. A
realizability interpretation of the negative translation of the Axiom
of Choice.
Lecture 4: use of formal topology (constructive theory of locales) for
extracting constructive content from non-constructive
proofs. Application to the topological proof of van der Waerden's
theorem on arithmetical progression.
----------------------------------------------------------------------
Martin Hofmann (Edinburgh)
"Dependent type theory: syntax, semantics, and applications"
(4 lectures)
The aim of this course is to familiarise participants with the use of
dependent types from the viewpoint of their categorical
semantics. Dependent types are types depending on values, for instance
lists of a fixed length (arrays), the type of constructive proofs of a
fixed proposition, the type of certain algebraic structures over a
fixed set, etc. Categorical semantics provides a general framework
for formulating and verifying interpretations of dependent types.
The course will start with an introduction to theories of dependent
types covering Martin-Lof's type theory, the Logical Framework,
and the Calculus of Constructions. Guided by syntactic intuition we
develop the notion of "categories with families", a simple yet
sufficiently general notion of categorical semantics, and define the
interpretation of the syntax therein. We then look at some instances
such as term models and realisability models and compare to other
semantic notions, in particular models based on fibrations. Finally,
we treat some larger applications from Computer Science, such as
Paulin-Mohring's method of program extraction from proofs, Moggi's
work on semantics of modules, and the groupoid interpretation of
Martin-Lof's type theory.
----------------------------------------------------------------------
Martin Hyland (Cambridge)
"Game Semantics"
(4 lectures)
course content t.b.a.
----------------------------------------------------------------------
Eugenio Moggi (Genova)
"Computational types and applications"
(4 lectures)
The prerequisites for this course are some knowledge of typed lambda
calculus and equational logic. I will avoid use of domain theory as
much as possible, because the basic ideas do not rely on it. However,
the more sophisticated examples will have to make use of it.
Lecture 1: Computational types -- syntax and equations.
Lecture 2: Examples of computational types in the category of sets.
Lecture 3: Semantics of programming languages via translation into a
metalanguage with computational types; examples.
Lecture 4: Modular approach to denotational semantics via
reinterpretation of computational types.
----------------------------------------------------------------------
Mogens Nielsen & Glynn Winskel (Aarhus)
"Models for concurrency"
(4 lectures)
In these lectures we will highlight a selection of the mathematical
structures used in modelling parallel computation, ranging from
"interleaving" models like transition systems to models like Petri
nets and Mazurkiewicz traces, where concurrency is represented more
explicitly by a form of causal independence. The presentation is
unified by casting the models in a category-theoretic framework.
Category theory is used to provide abstract characterisations of
constructions like parallel composition, and broadly applicable
definitions of bisimulation, valid throughout a range of different
models. In addition, category theory yields formal means for
translating between different models.
----------------------------------------------------------------------
Andrew Pitts (Cambridge)
"Operationally-based theories for proving program properties"
(3 lectures)
The aim of the lectures will be to describe recent advances in
techniques based on operational semantics for establishing equivalence
of programs. The co-inductive characterization of contextual
equivalence between functional programs in terms of "applicative
bisimulation" will be presented. The use of co-induction for reasoning
about lazy datatypes will be illustrated. The extent to which this
characterization generalizes to "impure" functional languages will be
discussed.
======================================================================
LOCATION
The workshop will take place in the Newton Institute's purpose
designed building, in a pleasant area in the west of Cambridge, about
one mile from the centre of the City. Accommodation for participants
will be provided next door to the Newton Institute in the study
bedrooms of Girton College's Wolfson Court. The accommodation will be
available from the evening of Sunday 24 September until the morning of
Saturday 30 September.
Fees:
general rate: 400 pounds
student rate: 250 pounds
The fee covers registration, accommodation, meals (breakfast, lunch,
supper, tea & coffee breaks), and lecture materials.
REGISTRATION
There are only a limited number of places available on the Summer
School. Intending participants are advised to apply for registration
as soon as possible, and in no case later than 30 June 1995. To apply,
please send your name and address (including e-mail or fax number, if
available) to:
Florence Leroy
(SEM Summer School)
Isaac Newton Institute
20 Clarkson Road
Cambridge CB3 0EH
Tel: +44 1223 335984
Fax: +44 1223 330508
Email: f.leroy@newton.cam.ac.uk
ORGANIZERS
For CLICS-II: Peter Dybjer (Chalmers)
peterd@cs.chalmers.se
For the NIMS Semantics of Andrew Pitts (Cambridge)
Computation Programme: ap@cl.cam.ac.uk
IMPORTANT DATES
(Revised) deadline for registration 30 June 1995
Arrival date 24 September 1995
Scientific programme 25--29 September 1995
Departure date 30 September 1995
---------------------------------------------------------------------------