From applicative to environmental bisimulation

Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)

Abstract

We illuminate important aspects of the semantics of higher-order functions that are common in the presence of local state, exceptions, names and type abstraction via a series of examples that add to those given by Stark. Most importantly we show that any of these language features gives rise to the phenomenon that certain behaviour of higher-order functions can only be observed by providing them with arguments which internally call the functions again. Other examples show the need for the observer to accumulate values received from the program and generate new names. This provides evidence for the necessity of complex conditions for functions in the definition of environmental bisimulation, which deviates in each of these ways from that of applicative bisimulation.

Original languageEnglish
Pages (from-to)215-235
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume276
Issue number1
DOIs
Publication statusPublished - 2011 Sep 29

Keywords

  • Environmental bisimulation
  • applicative bisimulation
  • existential types
  • local state

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'From applicative to environmental bisimulation'. Together they form a unique fingerprint.

Cite this