|
|
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) =
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:
()