From applicative to environmental bisimulation

Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii

Research output: Contribution to journalArticlepeer-review

26 Citations (Scopus)


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
Issue number1
Publication statusPublished - 2011 Sept 29


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


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

Cite this