Abstracts of the tutorials at the Winter Workshop in Logics, Types and Rewriting

Cedar Room, Heriot-Watt University, Edinburgh

1-3 February 2000


ULTRA logo ULTRA group
Useful Logics, Types, Rewriting,
and Applications
UK Institute of Informatics,

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