Abstracts of the tutorials at the Winter Workshop in Logics, Types and Rewriting
Cedar Room, Heriot-Watt University, Edinburgh
1-3 February 2000
 |
http://www.cedar-forest.org/forest/events/inaugural-workshop2000/ina-abstracts1.html
 |
ULTRA group
Useful Logics, Types, Rewriting,
and Applications |
 |
HEIGHT=43 WIDTH=89>
UKII
UK Institute of Informatics,
UK |
The list of abstracts of the tutorials is as follows:
Mirna Bognar Free University of Amsterdam
A calculus of contexts: part I
This tuturial is about contexts, i.e. expressions
with special places, called holes, where other expressions can be placed.
In formal systems with bound variables,
a distinctive feature of placing an arbitrary expression
into a hole of a context is variable capturing: some
free variables of the expression
may become bound by the binders of the context.
We will explain the problems that arise
when manipulating contexts on the same level as expressions,
give an overview of calculi with contexts, and
propose a uniform representation of multiform contexts.
Sophia Drossopoulou Imperial College, London
Towards a model of dynamic linking and verification for Java
We develop a high level model which describes dynamic linking,
verification and execution as in Java. The model distinguishes
between execution, loading, verification and linking and
the corresponding associated four kinds of checks; it demonstrates
their dependencies, and how together they guarantee type soundness.
The model is high level: it is based on a language nearer to Java
source than the byte-code; thus it is independent from the particular
byte-code.
Alan Mycroft Computer Laboratory, Cambridge University
A Statically Allocated Parallel Functional Language
Joint Work with Richard Sharp (AT&T Laboratories Cambridge),br>
We describe an eager higher-order functional language (SAFL)
in the style of ML which
is syntactically (and by typing rules) restricted so that storage,
including input and output values, may be statically allocated.
This means that it can be used as a hardware description language.
Argument evaluation occurs natually
in parallel but we can associate function definitions with physical resources
protected by semaphores (arbiters or timing analysis in hardware).
in a manner which preserves static allocation.
The difference between optimisations to improve hardware and those
to improve software is neatly highlighted by this langyage.
We can see fold/unfold transformations as being maps between space
and time resources (cf.\ the area-time lower bound from VLSI design).
The space of functions expressible is incomparable with the
space of primitive recursive functions, in particular an
interpreter for register machines may be expressed.
Adolfo Piperno
University of Roma
A new approach to the problem of discriminability
We briefly review recent works about Boehm trees and
we present an algebraic approach to the discriminability problem
in untyped lambda-calculus.
Dr Roel C. de Vrijer
Free University of Amsterdam
A Context calculus: part II
Same abstract as Part I.
Jan Zwanenburg Catholic University of Nijmegen
Pure Type Systems and Subtyping
The tutorial starts with a brief description of Pure Type Systems and
some existing type systems with subtyping. Then we discuss the main problem
appearing when Pure Type Systems are combined with subtyping, and our solution
to this problem. The result is a framework of Pure Type Systems with Subtyping,
containing both existing systems with subtyping and interesting new systems.
Maintained by
Fairouz Kamareddine
(
)
