Ian Stark

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

Andrew Pitts and Ian Stark

In Mathematical Foundations of Computer Science: Proceedings of the 18th International Symposium MFCS '93, Gdansk, Poland, August 30–September 3, 1993. Lecture Notes in Computer Science 711, pages 122-141. Springer-Verlag, 1993.

Fetch a preprint of the paper (PDF, 224k). Go to other papers, talks or my home page.

Abstract

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.

@InProceedings{pitts/stark:obspho-mfcs,
  author =       {Andrew M. Pitts and Ian Stark},
  title =        {Observable Properties of Higher Order Functions that
                  Dynamically Create Local Names, or: What's {\em new}?},
  booktitle =    {Mathematical Foundations of Computer Science:
                  Proceedings of the 18th International Symposium
                  MFCS~'93},
  pages =        {122--141},
  year =         1993,
  number =       711,
  series =       {Lecture Notes in Computer Science},
  publisher =    {Springer-Verlag},
  url =          {http://www.inf.ed.ac.uk/~stark/obspho-mfcs.html},
  pdf =          {http://www.inf.ed.ac.uk/~stark/obspho-mfcs.pdf}
}
Page last modified: Thursday 27 November 2008