International School on Type Theory and Term Rewriting

Glasgow University Sept 12-15 1996

ULTRA logo ULTRA group
Useful Logics, Types, Rewriting,
and Applications
UK Institute of Informatics,
The Engineering and Physical Sciences Research Council (EPSRC)

In the past twenty years, a very rich body of results has emerged in type theory and term rewriting systems. This is unsurprising since these topics are at the heart of the theory and implementation of programming languages. Type theory enables increasing expressiveness in programming languages and in theorem proving, whilst retaining strong theoretical and applied properties. Understanding termination and reduction strategies in term rewriting systems provides insights into increasingly efficient implementations with safe theoretical foundations. Furthermore, the two notions of type theory and term rewriting are very general and cover various topics including termination, calculi of substitutions, subtyping, reduction, unification, interaction and process calculi, the logic of programs and theorem proving.

Unfortunately, collaboration between type theory and term rewriting systems is not as strong as it should be despite their common goals and extreme importance. The International School on Type Theory and Term Rewriting aims at bridging this gap and at bringing together leaders and active researchers in the various branches of type theory and term rewriting. The school is beneficial to all active researchers and research students in the area. Talks will range from an overview of recent results, to presenting some open problems and to discussing some future research in the area. The list of invited speakers includes: Jos Baeten, Steffen van Bakel, Henk Barendregt, Gilles Barthe, N.G. de Bruijn, Roberto Di Cosmo, Michael Fourman, Herman Geuvers John Glauert, Thérèse Hardin, Fairouz Kamareddine, Richard Kennaway, Assaf Kfoury, Zurab Khasidashvili, Jan Willem Klop, Pierre Lescanne, Jean-Jacques Lévy, Giuseppe Longo, Ursula Martin Paul-André Melliès, Cristine Paulin-Mohring, Adolfo Piperno, Gordon Plotkin, Alejandro Ríos, Simona Ronchi Della Rocca, Judith Underwood, Roel de Vrijer, Joe Wells.

Here is the list of Participants. Here are some photos from the school.

Here is the Programme:

|-----------------------------------| |-----------------------------------|
|Thursday 12 September              | |Friday 13 September                |
|-----------------------------------| |-----------------------------------|
|   Chair: Fairouz Kamareddine      | |   Chair: Jan-Willem Klop          |
|   --------------------------      | |   ----------------------          |
|   9:00- 9:45 N.G. de Bruijn       | |   9:00- 9:45 Therese Hardin       |
|   9:45-10:00 Discussion           | |   9:45-10:00 Discussion           |
|                                   | |                                   |
|  10:00-10:45 Henk Barendregt      | |  10:00-10:45 Michael Fourman      |
|  10:45-11:00 Discussion           | |  10:45-11:00 Discussion           |
|                                   | |                                   |
|  11:00-11:30 COFFEE BREAK         | |  11:00-11:30 COFFEE BREAK         |
|                                   | |                                   |
|  Chair: Roy Dyckhoff              | |  Chair: Zhaoui Luo                |
|  -------------------              | |  -----------------                | 
|  11:30-12:15 Fairouz Kamareddine  | |  11:30-12:15 Joe Wells            |
|  12:15-12:30 Discussion           | |  12:15-12:30 Discussion           |
|                                   | |                                   |
|  12:30-14:00  LUNCH               | |  12:30-14:00  LUNCH               |
|                                   | |                                   |
|  Chair: Randy Pollack             | | Chair: Franco Barbanera           | 
|  --------------------             | | -----------------------           |
|  14:00-14:30 Gilles Barthe        | |  14:00-14:45 Jean-Jacques Levy    |
|  14:30-15:00 Alejandro Rios       | |  14:45-15:00 Discussion           |
|                                   | |                                   |
|  15:00-15:30 Herman Geuvers       | |  15:00-15:30 Paul-Andre Mellies   |
|                                   | |                                   |
|  15:30-16:00 COFFEE BREAK         | |  15:30-16:00 COFFEE BREAK         |
|                                   | |                                   |
|  Chair: Steffen van Bakel         | |  Chair: Pierre Lescanne           |
|  ------------------------         | |  ----------------------           |
|  16:00-16:45 Jos Baeten           | |  16:00-16:45 Gordon Plotkin       |
|  16:45-17:00 Discussion           | |  16:45-17:00 Discussion           |
|-----------------------------------| |-----------------------------------|

|-----------------------------------| |-----------------------------------|
|Saturday 14 September              | |Sunday 15 September                |
|-----------------------------------| |-----------------------------------|
|   Chair: Maribel Fernandez        | |  Chair: Adriana Compagnoni        |
|   -------------------------       | |  -------------------------        |
|   9:00- 9:45 Pierre Lescanne      | |  9:00- 9:45 Giuseppe Longo        |
|   9:45-10:00 Discussion           | |  9:45-10:00 Discussion            |
|                                   | |                                   |
|  10:00-10:30 Steffen van Bakel    | |  10:00-10:45 Adolfo Piperno       |
|  10:30-11:00 Roel de Vrijer       | |  10:45-11:00 Discussion           |
|                                   | |                                   |
|  11:00-11:30 COFFEE BREAK         | |  11:00-11:30 COFFEE BREAK         |
|                                   | |                                   |
|  Chair: Paul Jackson              | |  Chair: Olivier Danvy             |
|  -------------------              | |  --------------------             | 
|  11:30-12:15 Christine Paulin     | |  11:30-12:15 Ursula Martin        |
|  12:15-12:30 Discussion           | |  12:15-12:30 Discussion           |
|                                   | |                                   |
|  12:30-13:00 Judith Underwood     | |  12:30-13:00 John Glauert         |
|                                   | |                                   |
|  13:00-14:00  LUNCH               | |  13:00-14:00  LUNCH               |
|                                   | |                                   |
|  Chair: Kristoffer Rose           | |  Chair: Ursula Martin
|  ----------------------           | |  ------------------------         |
|  14:00-14:45 Jan-Willem Klop      | |  14:00-14:45 Richard Kennaway     |
|  14:45-15:00 Discussion           | |  14:45-15:00 Discussion           |
|                                   | |                                   |
|  15:00-15:30 Roberto Di Cosmo     | |  15:00-15:30 Zurab Khasidashvili  |
|                                   | |                                   |
|  15:30-16:00 COFFEE BREAK         | |  15:30-16:00 COFFEE BREAK         |
|                                   | |                                   |
|  Chair: Henk Barendregt           | |  Chair: Philippe Audebaud         | 
|  ----------------------           | |  ------------------------         |
|  16:00-16:45 Assaf Kfoury         | |  16:00-16:45 S. Ronchi Della Rocca|
|  16:45-17:00 Discussion           | |  16:45-17:00 Discussion           |
|-----------------------------------| |-----------------------------------|

Here are the abstracts:

		Sequential data algebra
			Jos Baeten
		Eindhoven university of technology
(joint work with Jan Bergstra (Univ. of Amsterdam and Utrecht) and Alex
Sellink (Univ. of Amsterdam))

We propose a style of data type specification based on four valued logic.
Four valued logic has constants for true, false, meaningless and divergent;
this allows to deal with error values and non-terminating computations. The
word sequential indicates that all operators come with a definite order of
evaluation, thus a normalization strategy. The aim is to avoid endless
duplication and reinvention in the practice of algebraic specification.
As an example, we study the specification of floating-point numbers.
	Normalisation and approximation results for term rewriting systems 
	(with abstraction and \beta-rule) typeable using intersection types.
			Steffen van Bakel
			Imperial college, London
Research preformed in cooperation with Maribel Ferna'ndez, of E'cole Normale
Supe'rieure, Paris, and Franco Barbanera, University of Turin, Italy.

The talk will start with a short discussion of intersection type assignment
for Lambda Calculus, together with its major properties:
 - a filter model,
 - a strong normalization result,
 - a head-normalization result,
 - an approximation theorem.
We are interested in defining a filter-like semantics for other computational 
models, and our starting point was to have a look at first order term rewriting
systems.  We start with the definition of a notion of type assignment for
first order rewrite systems, extended with a notion of application, for
which we proved a subject reduction result.
We will present the restictions put on recursive definitions in order to
obtain the strong normalization and the head-normalization results.  We then 
will define a notion of approximants for terms in our rewrite system; the same 
restrictions as before on recursion are also sufficient for the approximation 
result. We then look at a calculus that combines term rewriting and 
beta-reduction, for which similar results are obtainable.
	Efficient Computations in Formal Proofs
		Henk Barendregt
	Catholic university of Nijmegen
Formal proofs in mathematics and computer science are being
studied because these objects can be verified by a very simple computer
program. An important open problem is whether
these formal proofs can be generated with an effort not much greater
than writing a mathematical paper in, say, \LaTeX. 
Modern systems for proof-development make the formalization of
reasoning relatively easy. Formalizing computations such that the
results can be used in formal proofs is not immediate.
In this talk it is shown how to obtain formal proofs of
statements like $\mathsf{Prime}(\num{61})$ in the context of Peano
arithmetic or $x^2-1=(x-1)(x+1)$ in the context of rings. It is hoped
that the method will help bridge the gap between systems of computer
algebra and systems of proof-development.
		 Classical Pure Type Systems
		  	Gilles Barthe
			CWI, Amsterdam
Since Griffin discovered that natural deduction systems for classical 
logics correspond to typed lambda-calculi with control operators via the 
Curry-Howard isomorphism, many such systems have appeared.

We introduce classical pure type systems (CPTSs), a framework
enabling a general study and systematic classification of such
calculi; akin to Barendregt's lambda-cube, we also define a 
classical lambda-cube, whose most complex system is a Classical
Calculus of Constructions. 

We briefly sketch the meta-theory of CPTSs: confluence, subject reduction, 
strong normalisation.  We also discuss a CPS-translation from the
clasical lambda-cube to Barendregt's lambda-cube.
		Features of Automath
		N.G. de Bruijn.
		Eindhoven University of Technology
Various proof verification systems, at least those
which combine typed lambda calculus with the idea of
proof objects, have much in common with old Automath. But
Automath has some features that were not taken over by
others and nevertheless have technical and conceptual
advantages.  In particular this refers to the book
structure of PAL, the lambda-free fragment of Automath.
Instead of replacing that structure by lambda formalism,
Automath maintained it, thus providing a double mechanism
for functionality. One of the effects of keeping the PAL
structure is the natural way to internalize definitions, a
thing that has to be given up if the PAL mechanism is
replaced by typed lambda calculus. It can be reclaimed if
ordinary typed lambda calculus is replaced by the only
slightly different modification called delta-lambda.
	A brief history of rewriting with extensionality
		Roberto Di Cosmo
		Ecole Normale Superieure, Paris
Over the past years, much work has been done on typed lambda
calculi with extensional axioms turned into expansive rules
rather than into contractive ones. We will survey the rewriting
techniques that have been developed and used for these calculi,
which are a typical example of fruitful interaction between
lambda calculus and rewriting, and we will survey also the most
recent results in the field.
		Indeterminate Structures
		Michael Fourman
		The University of Edinburgh
We use the notion of a generic object, from topos theory, to model
indeterminate types.
This allows us to give a semantics for SML functors. We describe the
construction of indeterminate
structures, used to model functor parameters, and discuss the features of a
module system based on this semantics.
	From models of logic to models of typed lambda calculus
			Herman Geuvers
		Tech. University Eindhoven, NL
Abstract: Type theories with type dependency, like the Calculus of
Constructions, can be used for formalizing mathematical reasoning,
using the formulas-as-types principle, which embeds a logic
into the type theory. Hence, when implemented, such a type theory can
be used as an interactive proof checker. Then it also becomes apparent
that pure logic is a rather `static' thing: functions are usually seen
as relations and hence do not compute. Also, formalising things in
pure logic involves a lot of coding. These drawbacks can be improved
in type theory by allowing additional constructs (like, for
example, lambda-abstraction, or a scheme for inductive types). Type
theory also allows to formalize principles that can not be formalized
in ordinary logic, for example the idea that propositions and sets
are really the same kind of things (types), living in the same universe.

A question that arises here is what all these extra constructs and new
principles mean for the logic (e.g. are they conservative extensions?)
We look at this question by studying how a model of the logic can be
extended to a logic of the type theory. In detail we look at extending
(classical) models of second order logic to models of second order
dependent type theory.
		Neededness and Relative Normalization
			John Glauert
			University of East Anglia
(This work is performed in the context of Expression Reduction Systems, a
form of higher-order rewriting, and is joint work with Z. Khasidashvili.)

Practical applications of rewriting systems often require reduction to
head-normal forms or other classes of "normal" form. We generalize the
theory of normalization via neededness to normalization relative to
desirable sets of terms, S, having natural properties of stability which
guarantee normalization, whenever possible, by contraction of S-needed
redexes. We also discuss minimal and optimal needed reduction and show that
they need not coincide.
			What about freeness?
			Therese Hardin
In calculi with binders, variable names are well-known to be a source
of problems and De Bruijn notation, which replaces names by numbers
recording bindings, is a recognized way to avoid these
difficulties. It is easy to replace bound variables by numbers. Free
variables can also be replaced by numbers, by implicitly closing the
term but they may also be kept as names. We compare these two points
of view and we explain to code these free variables by metavariables
in a calculus of explicit substitutions. Then, we show how this coding
may be fruitfully used for unification and compilation.
		Type Theory and term Rewriting at Glasgow: Past and Future
			Fairouz Kamareddine
			University of Glasgow
This talk describes some of the problems attacked by the type theory and term 
rewriting group at Glasgow in the last five years and outlines some open 
problems and future goals.  The discussion will be directed towards implicitly
versus explicitly typed lambda calculi and the study of their theory and 
implementation.  I shall concentrate on extending those calculi with explicit 
definitions, explicit substitutions, new notions of typing and reductions
and the logical systems based on these calculi.   I will also be looking for
future generalisations of this work and its advantages.  For example, the
various new notions of reductions can be generalised even FURTHER and this
generalisation can provide a decidable charaterisation which is the nearest
approximation to the undecidable notion of reductional equivalence between 
terms.  It is very interesting indeed that almost all new  notions of 
reductions that have been found in the last twenty years by various 
researchers (as Bloo and Kamareddine and Nederpelt, Kamareddine and Nederpelt, 
Kfoury and Wells, Klop, Moggi, Nederpelt, Plotkin, Regner, etc), were trying
to remain within this notion of reductional equivalence.  

I shall outline the future I forsee for the type theory and
term rewriting group at Glasgow both within Glasgow and at the various 
centres with whom we collaborate. 
			Transfinite rewriting
			Richard Kennaway
			University of East Anglia
We survey the basic concepts and properties of transfinite rewriting for
orthogonal term rewrite systems, lambda calculus, higher-order rewrite
systems, and abstract rewrite systems.
		A Linearization of the Lambda-Calculus and Applications
			Assaf Kfoury
			Boston University
If every lambda-abstraction in a lambda-term M binds at most one variable 
occurrence (M is thus a ``linear'' term), then M is beta-strongly normalizing.
We extend the syntax of the standard lambda-calculus "Lambda" to adapt this 
idea to the general case when lambda-abstractions are allowed to bind more 
than one variable occurrence.

In the extended calculus, denoted "Lambda/\", a subterm Q of a term M can be
applied to several subterms R1,...,Rk in parallel, which we write as 
(Q. R1/\..../\Rk)$. The appropriate notion of beta-reduction "beta/\" for 
this extended calculus is such that, if Q is the lambda-abstraction 
(\lambda x.P) with l>= 0 bound occurrences of x, the reduction can be carried 
out provided k = \max(l,1). Every M in Lambda/\ is thus beta/\-SN. The 
contraction of M in Lambda/\ is a standard term |M| in Lambda, which is 
defined provided for every subterm of the form (Q. R1/\..../\Rk) =< M, each 
of R1,...,Rk contracts to the same standard term |R1| = ... = |Rk|. We say 
that M in Lambda/\wedge is "fully linear" if the beta/\wedge-normal form N 
of M is such that |N| is defined and is a standard term in beta-normal form.

One key lemma states that for every standard term M in Lambda:
M is beta-SN iff there is a fully linear M' in Lambda/\ such that M = |M'|. 
We draw several consequences from this result, in particular a new simple 
proof for the (known) fact that a (standard) term M is beta-SN iff M can be 
assigned a so-called ``intersection'' type (``top'' type disallowed).
	Comparing stable models of deterministic computation
		Zurab Khazidashvili
		University of East Anglia
(This work has been performed in cooperation with John Glauert.)

Event Structures are well established models of concurrent computation.
Here we study Event Structure semantics for Orthogonal Rewrite Systems,
such as the lambda-calculus and its sharing graph model, and of functional
programming languages based on such systems. Conflict-free (or Deterministic) 
Prime Event Structures, DPESs, which are simply event sets partially ordered 
by a causal dependency relation, are sufficient for this purpose.

We study orthogonal systems in the form of Stable Deterministic Residual
Structures (SDRSs), which are Abstract Reduction Systems with axiomatized
residual relation. Basic theory of orthogonal systems, such as
normalization, can be developed already in the framework of SDRSs. In order
to interpret SDRSs as DPESs, an equivalence relation on transitions in
SDRSs is required that would relate transitions performing (part of) the
`same' event. We introduce such structures, Deterministic Family Structures
(DFSs), by axiomatizing family relation on transitions in SDRSs, by analogy
with the family relation in the lambda calculus and other orthogonal
rewrite systems. DFSs can easily be interpreted as DPESs (by taking
redex-families as events and taking the contribution relation on them as
the causal dependency relation on events).

However, DPESs are linear in nature (no event can erase or duplicate
another -- any event can occur at most once in the course of a computation), 
and therefore they cannot give an adequate account of erasure of redexes/
transitions in SDRSs. To remedy this situation, we extend DPESs in two ways: 
by axiomatizing erasure relation on events, and by axiomatizing permutation 
equivalence on event configurations. We then define translations between the 
two extended event models, non-duplicating SDRSs, and non-duplicating DFSs, 
and show that the translations commute, implying isomorphism of the above 
set-theoretic and transition models of deterministic computation.
		Decreasing diagrams
		Jan Willem Klop
		CWI and Vrije Universiteit, Amsterdam
	Joint work with Marc Bezem and Vincent van Oostrom.

We discuss confluence criteria for abstract rewriting, notably the method of 
decreasing diagrams due to De Bruijn and van Oostrom. This method generalizes
various lemma's in abstract rewriting such as Newman's Lemma, Huet's strong 
confluence lemma and several others. We also pay attention to infinite 
reduction diagrams.
		Pierre Lescanne
		Inria, Nancy
Calculi of explicit substitution internalise the main process of
lambda-calculus, namely substitution. Thus substitution is better
understood and its complexity is better mastered.  Actually calculi of
explicit substitution can be divided into two classes, namely those
which use de Bruijn's indices and those which use names.  It is well
known that de Bruijn's indices make terms less readable and therefore
names are often prefered by people.  But when one uses names, one is
faced to the problem of alpha conversion which is is somewhat hidden
in de Bruijn's indices and one may like to make it explicit either. We
propose a calculus which uses a convention for attributing names based
on their binding depth and introduced as ``levels'' by de Bruijn in
1972.  Thanks to levels, alpha conversion can be made explicit in our
calculus.  We discuss some of its properties and applications.
		Dependency calculus for the lambda calculus.
			Jean-Jacques Levy
			Inria, Paris
Vesta is a modeling system with a functional language for
describing software packages. Incremental calculation of dependencies
may be viewed as a simple lambda calculus problem, with an extra
origin calculation. Joint work with Abadi and Lampson.
		Giuseppe Longo
		Ecole Normale Superieure, Paris
A recent logical theory of subtypes is introduced.  Its motivation 
goes back to the introduction, in a functional frame, of a typical  
Object Oriented feature, inheritance, reinterpreted in a specific  
and functional, way.  The presentation in terms of sequent calculi  
allows to formulate and prove a coherence theorem and a  
"transitivity elimination" result.  The later may be handled as a  
cut-elimination (normalization) result, in the sense of logic.  The  
implicit challenges will be shortly discussed.  The analysis of  
cut-elimination and of "injectivity" of subtyping relates to an 
apparently unrelated result on parametricity of higher order  
lambda-calculi, which in turn gives some insight into the proof of  
		Termination, geometry and invariants
			   Ursula Martin
			University of St Andrews
Many different techniques have been developed for proving the termination
of programs or functions. Some are purely ad-hoc arguments developed solely
to solve an immediate problem. However a typical termination proof involves
finding a quantity which decreases at each step of a computation, or in
other words finding a well-founded ordering which is respected by the process 
we are considering.  An extraordinary diversity of well-founded division 
orderings on structures such as vectors, strings, partitions or terms have 
been devised to prove termination, particularly of rewrite systems.

Such orderings can also be used to constrain the search space in the search
for solutions or normal forms in a wide variety of algorithms such as Knuth
Bendix completion, for computation in algebras or groups,  Gr\"{o}bner
basis, for computation in polynomial rings, or resolution. It turns out
that the choice of ordering may have a surprising effect on efficiency.

Recent work has shown that in some circumstances a geometrical classifying
space for the orderings may be found, which allows us to associate
invariants to the orderings and the associated termination problems. We
discuss theorems, examples and questions.
		The lambda sigma calculus is omega deterministic
			Paul-Andre Mellies
		LFCS, University of Edinburgh
The normalisation in the lambda calculus of (fair) call-by-need strategies 
is a consequence of the standardisation theorem.
The demonstration is extended here to non commutative (= non orthogonal) 
rewriting systems. First we characterise algebraically the subclass of 
``external'' computations inside reduction systems --- a subclass which 
contains all normalising computations. Then we reduce the normalisation 
property to the finite number of permutation classes, see Jean-Jacques 
Levy's Phd, from a term to its several normal forms --- what we call 
omega-determinism. Finaly we show that the lambda sigma calculus enjoys 
the property: as a consequence all (fair) call-by-need strategies 
in the lambda sigma calculus are normalising.
	Inductive Types in Higher-Order Logic and Type Theory
	Christine Paulin-Mohring 
	LIP, URA CNRS 1398, ENS Lyon, France
Inductive types and definitions are an important tool when formalising 
mathematical concepts. Impredicative systems such that higher-order logic 
or impredicative type theories offer the possibility to encode these objects.
We present a comparative approach of these encodings with respect to the 
class of inductive types that are representable and the 
properties that are provable on them.  We shall present more precisely the 
inductive types as they are represented in the Coq system.
	Normalization by developments and subtyping
		Adolpho Piperno
		University of Roma
Normalization proofs for typed lambda-calculi have received
a considerable interest in the last few years.
In particular, investigations have been made to clarify
the relationship between weak and strong normalization, 
to refine the notion of development and to give
syntactical tools for studying properties of reduction.
Some of these issues will be reviewed and discussed.
A general method for proving normalization
in typed lambda calculi will be presented, based on the 
use of eta-expansions, superdevelopments and subtyping. 
	Compositionality and Universal Type Theory
			Gordon Plotkin
		University of Edinburgh
The principle of compositionality or referential transparency is central to
denotational semantics.  Taking this seriously requires a theory of
language.  For example, viewing language as a free multi-sorted algebra
enables one to express compositionality homomorphically, as advocated long
ago by the ADJ group.  It also provides a uniform notion of translation
between signatures that allows one to pass from the semantics of one
language to that of another.

However such a theory of language is inadequate, and for several reasons.
We consider two of these: the lack of a treatment of binding operators, and
the fact that sorts (= types), can themselves have a complex linguistic
structure.  Making a (partial) identification of type theories with
programming languages, we advocate a programme to find a treatment of type
theories analogous to the universal algebraic treatment of algebraic
theories.  With this, the language used to express (typically)
domain-theoretic semantics is itself brought into the picture, and one can
see compositional denotational semantics itself as translation, in a
uniform sense.
           Two styles of explicit substitutions: a survey
                    Alejandro Rios
                    University of Glasgow
(This work is carried out in collaboration with Fairouz Kamareddine and is
supported by EPSRC grant GR/K25014: "Theoretical and implementational 
advantages of a new lambda notation".)

Most formulations of the lambda-calculus use implicit rather than explicit
substitutions. The last decade however has seen an explosion of calculi  
which deal with substitutions explicitly.

This talk starts by giving a brief introduction to two different styles of 
explicit substitutions: the already classical lambda-sigma style and the 
recently developped lambda-s style. We discuss substitutions calculi 
with de Bruijn indices and with variable names, try to establish a bridge 
between both and compare substitutions calculi in both styles from the point 
of view of efficiency to simulate beta-reduction.
Furthermore, for each style, we outline the remaining open problems and the 
disadvantages versus the advantages they offer.
	The operational content of intersection types
		Simona Ronchi Della Rocca
		Univerity of Turino
 Various aspects of the functional computation can be modeled 
 through (various kinds  of) lambda calculus. For example, the
 call-by-name computation, the call-by-value one, the lazy one,
 the relevant one. An operational semantics can be defined 
 for each one of these paradigmatic languages, starting from 
 the definition of a set of "values", and a notion of convergency.
 A term converges if and only if it reduces (according to a 
 given reduction strategy) to a value. A notion of operational 
 equivalence between terms arises naturally, based on Leibnitz equality.
 Namely two terms M and N are operationally equivalent if and only if  
 every context behaves in the same way (with respect
 to the convergency) when filled by either M or N.
 Intersection type assignment systems give a tool for reasoning 
 about operational equivalence of terms. We define a type assignment
 system being correct with respect to an operational equivalence
 if and only if the fact that two terms can be typed with the
 same types implies that they are operationally equivalent.
 If also the inverse implication holds the system will be called
 complete. For each one of the operational semantics induced by
 the before listed computations a correct type assignment system
 can be defined.  
	Classical logic and nonlocal control: the case against confluence
			Judith Underwood
		University of Edinburgh
Nonlocal control operators were introduced to functional languages to
allow programmers to guide the evaluation process more efficiently.
They can also be used to implement error handlers and concurrency
mechanisms such as coroutines.  However, they represent a significant
addition to the principles of lambda-calculus which underlie many
ideas in functional programming.  Furthermore, there appears to be a
deep connection between classical logic and typed lambda-calculus plus
nonlocal control, similar to the connection between constructive logic
and typed lambda-calculus.  

An important consideration in studying languages
with nonlocal control operators is that they may be nonconfluent.
This property can be justified both by the connection with classical
logic and by applications to programming.  Because of this,
many proof techniques for properties such as normalization
cannot be used directly.  It is hoped that this talk will motivate
work on such proof methods.
		Completing partial combinatory algebras
			Roel de Vrijer
		Free University of Amsterdam
	This is joint work with I. Bethke and J.W. Klop.

In this talk a over view will be given of the results on completability
of partial combinatory algebras. 
A short review  will be given of constructions by J.W. Klop and I. Bethke
of partial combinatory algebras that can not be completed.
On the other hand, we will prove that partial combinatory algebras having
the additional property of 'unique head normal forms', can always be completed.
An example is the 'Kleene brackets' pca with domain N and application defined
by n.m = {n}m.
		Generalized Reduction, Let-Floating, and CPS
				Joe Wells
  				Boston University
Generalized reduction recognizes implicit beta redexes in a lambda term
and reduces them directly, ignoring intervening abstractions and
applications.  Let-floating lifts or lowers beta redexes to other
equivalent locations.  A CPS transformation changes terms into a form
which is executable on a stack-based implementation and which is
indifferent to call-by-value vs. call-by-name evaluation.

We evaluate and survey different restrictions on let-floating.  We discuss
how generalized reduction is subsumed by a particular subset of
let-floating.  We show how a larger subset of let-floating is subsumed by
beta reduction on CPS transformed terms.  We discuss the application of
these techniques in such areas as type inference, strong normalization,
and program equivalence.

Registration fee is £ 150 (£ 75 for full time students).

Accommodation is available at the following rates per person per night:

Staff: £ 20.50 (bed and breakfast) or £ 11.50 (bed only).

Students (bed only): £ 8.50 (UK students) and £ 10.00 (overseas students).

If you are interested in attending, send the registration fee (with evidence of full time studentship if applicable), together with the fee for the accommodation for the relevant number of nights and type of accommodation to: Fairouz Kamareddine, Attention International School on Type Theory and Term Rewriting, Glasgow University, Computing Science, 17 Lilybank Gardens, Glasgow. Note that cheques must be made payable to Glasgow University and labelled: "International School on Type Theory and Term Rewriting".

Fairouz Kamareddine email: ()

Maintained by Fairouz Kamareddine email: ()