License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10351.5
URN: urn:nbn:de:0030-drops-28092
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2809/
Go to the corresponding Portal

Tzevelekos, Nikos

Program Equivalence with Names

pdf-format:
10351.TzevelekosNikos.Paper.2809.pdf (0.2 MB)

Abstract

The nu-calculus of Pitts and Stark was introduced as a paradigmatic
functional language with a very basic local-state effect: references of unit
type. These were called names, and the motto of the new language went as
follows:

"Names are created with local scope, can be tested for equality, and are
passed around via function application, but that is all."

Because of this limited framework, the hope was that fully abstract models
and complete proof techniques could be obtained. However, it was soon
realised that the behaviour of nu-calculus programs is quite intricate, and
program equivalence in particular is surprisingly difficult to capture. Here we
shall focus on the following "hard" equivalence.

new x,y in f. (fx=fy) == f. true

We shall examine attempts and proofs of the above, explain the advantages
and disadvantages of the proof methods and discuss why program
equivalence in this simple language remains to date a mystery.

BibTeX - Entry

@InProceedings{tzevelekos:DagSemProc.10351.5,
  author =	{Tzevelekos, Nikos},
  title =	{{Program Equivalence with Names}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2809},
  URN =		{urn:nbn:de:0030-drops-28092},
  doi =		{10.4230/DagSemProc.10351.5},
  annote =	{Keywords: Nu-calculus, Local State, Logical Relations, Game Semantics, Environmental Bisimulations}
}

Keywords: Nu-calculus, Local State, Logical Relations, Game Semantics, Environmental Bisimulations
Collection: 10351 - Modelling, Controlling and Reasoning About State
Issue Date: 2010
Date of publication: 04.11.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI