[Prev][Next][Index][Thread]

What's new?




With apologies for the Wadleresque alternate title, we would like to
announce the availability of the following paper:

                          **********************

                         Observable Properties of 
                        Higher Order Functions that 
                      Dynamically Create Local Names, 
                            or: What's new?

                        Andrew Pitts and Ian Stark

The research reported in this paper is concerned with the problem of 
reasoning about properties of higher order functions involving state. 
It is motivated by the desire to identify what, if any, are the 
difficulties created purely by _locality_ of state, independent 
of other properties such as side-effects, exceptional termination and 
non-termination due to recursion. We consider a simple language 
(equivalent to a fragment of Standard ML) of typed, higher order 
functions that can dynamically create fresh _names_; names are 
created with local scope, can be tested for equality and can be passed 
around via function application, but that is all. Despite the extreme 
simplicity of the language and its operational semantics, the 
observable properties of such functions are shown to be very subtle. A 
notion of `logical relation' is introduced which incorporates a 
version of _representation independence_ for local names. We 
show how to use it to establish observational equivalences. The method 
is shown to be complete (and decidable) for expressions of first order 
types, but incomplete at higher types.

                          **********************

The paper is available by anonymous ftp from theory.doc.ic.ac.uk
[146.169.22.150] in the directory papers/Pitts as

mfcs.{dvi,ps[.Z]}

This paper is an expanded version of the operationally-based results
announced in our paper to appear in the ACM SIGPLAN workshop on State
in Programming Languages (Copenhagen, June 1993). That reference also
contains an outline of our approach to the denotational semantics of
dynamic allocation of fresh names.  It resides in the above directory
as

sipl.{dvi,ps[.Z]}


Andrew Pitts
Ian Stark