License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-28074
URL: http://drops.dagstuhl.de/opus/volltexte/2010/2807/
Go to the corresponding Portal


Koutavas, Vasileios ; Levy, Paul Blain ; Sumii, Eijiro

Limitations of Applicative Bisimulation (Preliminary Report)

pdf-format:
Document 1.pdf (196 KB)


Abstract

We present a series of examples that illuminate an important aspect of the semantics of higher-order functions with local state. Namely that certain behaviour of such functions can only be observed by pro- viding them with arguments that contain the functions themselves. This provides evidence for the necessity of complex conditions for functions in modern semantics for state, such as logical relations and Kripke-like bisimulations, where related functions are applied to related arguments (that may contain the functions). It also suggests that simpler semantics, such as those based on applicative bisimulations where functions are ap- plied to identical arguments, would not scale to higher-order languages with local state.

BibTeX - Entry

@InProceedings{koutavas_et_al:DSP:2010:2807,
  author =	{Vasileios Koutavas and Paul Blain Levy and Eijiro Sumii},
  title =	{Limitations of Applicative Bisimulation (Preliminary Report)},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  year =	{2010},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  number =	{10351},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2807},
  annote =	{Keywords: Imperative languages, higher-order functions, local state}
}

Keywords: Imperative languages, higher-order functions, local state
Seminar: 10351 - Modelling, Controlling and Reasoning About State
Issue Date: 2010
Date of publication: 04.11.2010


DROPS-Home | Fulltext Search | Imprint Published by LZI