Jon Mountjoy | 3 Feb 17:21 1998


                        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 
      Types in Compilation

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

Sophia Drossopoulou | 4 Feb 14:51 1998

Research Associate Position on Java at Imperial College, LONDON

More information can be found at:
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

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
combination of fooling the byte-code verifier and the linker/loader.
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
(Continue reading)

Benjamin Pierce | 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:

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


        Martin Hofmann
        Benjamin Pierce


                          TYPE DESTRUCTORS

            Martin Hofmann               Benjamin C. Pierce
     Technische Hochschule Darmstadt     Indiana University

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

Jean-Yves GIRARD | 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[dvi.Z,ps.Z,ps.gz]

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.

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

Xavier Leroy | 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.

For more information, see

(Continue reading)

Adriana Compagnoni | 6 Feb 16:16 1998

Decidability of Higher-Order Subtyping via Logical Relations


We would like to announce the availability of our paper, Decidability
of Higher-Order Subtyping via Logical Relations, at

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

(Continue reading)

Andrew Pitts | 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

  Parametric Polymorphism and Operational Equivalence
  (Preliminary Version)

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


  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.

Sophia Drossopoulou | 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:

We are looking forward to any feedback.


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

             Java Binary Compatibility is Almost Correct

             David Wragg, Sophia Drossopoulou and Susan Eisenbach 
             February 1998 

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

fairouz | 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

        This workshop is organized in conjunction with RTA-98

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

Alex Simpson | 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

The LFCS provides an ideal environment for postgraduate research. The
first six months of postgraduate training are supported by a unique
postgraduate course on the theory of computation. In addition, there
are regular short courses on advanced research topics, and a number of
forums provide weekly research seminars. The LFCS is particularly strong
in the area of semantics of programming languages.

(Continue reading)