3 Feb 17:21 1998

### CALL FOR WORKSHOPS: ICFP'98


CALL FOR WORKSHOPS

The 3rd ACM SIGPLAN

International Conference on Functional Programming (ICFP '98)

Mt Washington Conference Center
Baltimore, Maryland, USA
27-29 September 1998

The third International Conference on Functional Programming provides a
forum for researchers, developers, teachers, as well as users who love
programming with functions. The conference combines the Lisp and Functional
Programming (LFP) conference and the Functional Programming and Computer
Architecture (FPCA) conference, and is sponsored by ACM SIGPLAN.

ICFP '98 seeks a small number of workshop organizers who are interested in
co-locating a workshop on a functional programming language or on a topic
related to functional programming (in the sense of the Call for Papers). In
the past ICFP (incl. LFP, FPCA) has been co-located with workshops on:

Teaching Introductory Courses with Functional Languages
ML
Scheme
Types in Compilation

The workshops will take place on Saturday, September 26, 1998. The
organizers should plan for half day or full day workshops.


4 Feb 14:51 1998

### Research Associate Position on Java at Imperial College, LONDON

More information can be found at:
http://www.doc.ic.ac.uk/situation.html#job3

The Department
==============
Imperial College London is one of the largest Colleges of the University
of London.  It currently has over forty full-time academic
staff, and is active in research on many topics including Logic and
Artificial Intelligence, Distributed Systems and Software Engineering,
Theory and Formal Methods, Advanced Languages and Architectures,
Computer Vision and Computer Graphics, Decision Support and Financial
Modelling, and Communicating Agents. It was rated 5* (the top rating)
in the most recent Research Assessment Exercise, and is also
rated Excellent in teaching.

The Research Project
====================
The research associate will be employed on the
SLURP: Sound Languages Underpin Reliable Programming
project.

The SLURP group is investigating the semantics of the Java language.
It has been demonstrated breaches of the Java security may be
originate with the possibility of breaking the type system through a
Previous work by the members gives a concise specification of a
substantial portion of the Java programming language and shows that the
type system is sound. That work is being extended to take in
environmental issues such as the effects of separate compilation,
dynamic linking,  the byte-code verifier and finally, to be able to


4 Feb 18:06 1998

### New technical report: Type Destructors

We are pleased to announce the availability of a new technical report
on "Type Destructors," available through:

http://www.cs.indiana.edu/hyplan/pierce/papers/td.ps.gz

This is an expanded version of the work that we presented at the FOOL
workshop a few weeks ago.

Enjoy,

Martin Hofmann
Benjamin Pierce

------------------------------------------------------------------------

TYPE DESTRUCTORS

Martin Hofmann               Benjamin C. Pierce

We study a variant of System Fsub that integrates and generalizes
several existing proposals for calculi with _structural typing rules_.
To the usual type constructors (->, #, All, Some, Rec) we add a number
of type _destructors_, each internalizing a useful fact about the
subtyping relation.  For example, in Fsub with products every closed
subtype of a product S#T must itself be a product S'#T' with S'<:S and
T'<:T.  We internalise this observation by introducing type
destructors .1 and .2 and postulating an equivalence T =eta T.1#T.2
whenever T <: U#V (including, for example, when T is a variable).  In
other words, every subtype of a product type literally _is_ a product


4 Feb 08:48 1998

### On the meaning of logical rules II

The paper "On the meaning of logical rules II : : multiplicatives and

is available at

ftp://iml.univ-mrs.fr/pub/girard/meaning1.[dvi.Z,ps.Z,ps.gz]

\begin{abstract}
El m\'etodo inicial que imagino era relativamente sencillo. Conocer
bien el espa\~nol, recuperar la fe cat\'olica, guerrear contra los
moros o contro el turco, olvidar la historia de Europa entre los
a\~nos de 1602 y de 1918, {\em ser} Miguel de Cervantes. Pierre
M\'enard estudi\'o ese procedimiento (s\'e que logr\'o un manejo
bastante fiel del espa\~nol del siglo diecisiete), pero lo descart\'o
por f\'acil. [\ldots]

Mi complaciente precursor no rehus\'o la colaboraci\'on del azar~:
iba componiendo la obra inmortal un poco {\em \a la diable}, llevado
por inercias del lenguaje y de la invenci\'on. Yo he contra\'{\i} el
misterioso deber de reconstruir literalmente su obra espont\'anea. Mi
solitario juego est\'a gobernado por dos leyes polares. La primera me
permite ensayar variantes de tipo formal o psicol\'ogico~; la secunda
me obliga a sacrificarlas al texto  \Guill{original} y a razonar de
un modo irrefutabile esa aniquilaci\'on.\\
J.-L. Borges {\em Pierre M\'enard autor del Quijote}, 1939.
\end{abstract}

The paper expounds the solution to our search for meaning
\cite{meaning1} in a particular case~: the fragment of logic built
from the neutral elements $\bot,\top$,${\bf 1},\bf 0$ by means of the


6 Feb 13:25 1998

### workshop Types in Compilation - call for participation

                 Advance program and call for participation

The Second International Workshop on

TYPES IN COMPILATION (TIC'98)

Advanced Compilation Techniques for Functional and Object-Oriented Languages

March 25-27, 1998
Kyoto, Japan

----------------------------------------------------------------------------

Types (in the broadest sense of the word) play a central role in many of the
advanced compilation techniques developed for modern programming languages.
Standard or non-standard type systems and type analyses have been found to
be useful for optimizing dynamic method dispatch in object-oriented
languages, for reducing run-time tests in dynamically-typed languages, for
guiding data representations and code generation, for program analysis and
transformation, for compiler verification and debugging, and for
establishing safety properties of distributed or mobile code. The "Types in
Compilation" workshops bring together researchers to share new ideas and
results in this area.

The next workshop, TIC'98, is a three-day meeting that will take place on
March 25-27, 1998, at Kyoto University. Formal proceedings will be published
in Springer-Verlag "Lecture Notes in Computer Science" series.



6 Feb 16:16 1998

### Decidability of Higher-Order Subtyping via Logical Relations


Hello,

We would like to announce the availability of our paper, Decidability
of Higher-Order Subtyping via Logical Relations, at
ftp://ftp.dcs.ed.ac.uk/pub/hhg/hosdec.ps.gz

The abstract for the paper is as follows:

This paper uses logical relations for the first time to study the
decidability of type-checking and subtyping.  The result is proved
for FOmegaSub, a language with higher-order subtyping and bounded
operator abstraction not previously known to be decidable.  The
proof is via an intermediate system called a typed operational
semantics, leading to a powerful and uniform technique for showing
metatheoretic results of type systems with subtyping, such as strong
normalization, subject reduction and decidability of subtyping.

Logical relations have been used for a wide variety of applications in
the syntax and semantics of type theory, for example strong
normalization following Tait and Martin-Lof, relating denotational and
operational semantics following Milne and Tait, Plotkin and others, or
operational equivalence as studied for example by Pitts.  The paper
exhibits a counterexample to show that the existing methods of Pierce
and Steffen and of Chen for showing decidability of subtyping do not
extend to the system with bounded operator abstraction.  Hence using
logical relations both gives a technique for showing new results, and
relates the study of subtyping to the wider body of results about type
theory.



6 Feb 16:56 1998

### parametric polymorphism and operational equivalence

See an old friend (polymorphic lambda calculus) in a new light by
reading the following preprint, available as

ftp://ftp.cl.cam.ac.uk/papers/ap/parpoe.ps

Parametric Polymorphism and Operational Equivalence
(Preliminary Version)

Andrew M. Pitts
Cambridge University Computer Laboratory
Pembroke Street, Cambridge CB2 3QG, UK

Abstract:

Studies of the mathematical properties of impredicatively
polymorphic types have for the most part focused on the
polymorphic lambda calculus of Girard-Reynolds, which is a
calculus of *total* polymorphic functions.  This paper
considers polymorphic types from a functional programming
perspective, where the partialness arising from the presence of
fixpoint recursion complicates the nature of potentially infinite
(lazy') datatypes.  An operationally-based approach to Reynolds'
notion of relational parametricity is developed for an extension of
Plotkin's PCF with forall-types and lazy lists.  The resulting
logical relation is shown to be a useful tool for proving properties
of polymorphic types up to a notion of operational equivalence based
on Morris-style contextual equivalence.


6 Feb 18:08 1998

### paper on Java Binary Compatibility

A paper discussing the concept an correctness of binary compatibility
in Java is available from:
http://outoften.doc.ic.ac.uk/projects/slurp/papers.html#bincomp

We are looking forward to any feedback.

Regards,

David Wragg, Sophia Drossopoulou, Susan Eisenbach.
--------------------------------------------------------- cut here

Java Binary Compatibility is Almost Correct
===========================================

David Wragg, Sophia Drossopoulou and Susan Eisenbach
February 1998

Abstract:
---------
The Java language description is unusual in that it defines
the effect of interleaving separate compilation and source code
modifications. In Java, certain source code modifications,
such as adding a method to a class, are defined as binary
compatible. The Java language  description does not require the
re-compilation of programs importing classes or interfaces which
were modified in binary compatible ways,  and it claims that
successful linking and execution of the altered  program
is guaranteed.

In this paper we show that Java binary compatibility does not


13 Feb 15:34 1998

### WESTAPP 98 -- International Workshop on Explicit Substitutions

                         WESTAPP 98

The First International Workshop on Explicit Substitutions:
Theory and Applications to Programs and Proofs

March 29, 1998, Tsukuba, Japan
CALL FOR PARTICIPATION AND EARLY
REGISTRATION

This workshop is organized in conjunction with RTA-98

http://www.dcs.gla.ac.uk/~fairouz/call.html

The aim of this workshop is to bring together researchers working on both the
theoretical and applied side of explicit substitutions, to present recent work
(possibly still in progress), and to discuss new ideas as well as emerging
trends in the following (not exclusive) topics:

+ New concepts in substitution calculi

+ Higher order types and explicit substitutions

+ Generalised techniques to show properties of substitution calculi

+ Relating explicit substitutions with other formalisms such as sequent
calculi, linear logic, game semantics, etc.

+ Accommodating different reduction strategies and control operators

+ Use of explicit substitution in proof checking and proof search, in


13 Feb 16:05 1998

### PhD Studentship at Edinburgh


Department of Computer Science
University of Edinburgh

Announcement of PhD Studentship in

Categorical Logic in Denotational Semantics

A PhD student is sought for three years from October 1998 to work
under the supervision of Dr. Alex Simpson on an EPSRC-funded project:
Categorical Logic and Structure in Denotational Semantics. The project
will apply category theory to axiomatize the essential structure of
denotational models of programming languages. The student will work on
the derivation of program logics from category-theoretic
axiomatizations, and on the proof-theoretical analysis of such logics.

The studentship is for three years and pays for all fees and includes
maintenance (living expenses) at the usual EPSRC rate.

The studentship will be held at the Laboratory for Foundations of
Computer Science (LFCS), Department of Computer Science, University of
Edinburgh.

The LFCS provides an ideal environment for postgraduate research. The
first six months of postgraduate training are supported by a unique