International School on Type Theory and Term Rewriting
International School on Type Theory and Term Rewriting
 |
ULTRA group Useful Logics, Types, Rewriting, and Applications |
 |
UKII UK Institute of Informatics, UK |
 |
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.
|-----------------------------------| |-----------------------------------| |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 | |-----------------------------------| |-----------------------------------|
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
INRIA, PARIS
-----------------------
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.
----------------------------------------------------------------------------
EXPLICIT SUBSTITUTIONS AND EXPLICIT ALPHA CONVERSION
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.
------------------------------------------------------------------------------
SUBTYPES, GENERICITY AND NORMALIZATION
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
normalization.
---------------------------------------------------------------------------
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:
()