Limitations of Applicative Bisimulation (Preliminary Report)

Authors Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii



PDF
Thumbnail PDF

File

DagSemProc.10351.4.pdf
  • Filesize: 195 kB
  • 9 pages

Document Identifiers

Author Details

Vasileios Koutavas
Paul Blain Levy
Eijiro Sumii

Cite As Get BibTex

Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. Limitations of Applicative Bisimulation (Preliminary Report). In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/DagSemProc.10351.4

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.

Subject Classification

Keywords
  • Imperative languages
  • higher-order functions
  • local state

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail