2026-07-21T14:13:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2809 2024-03-06T11:09:26Z ddc:004 open_access

Program Equivalence with Names Tzevelekos, Nikos Nu-calculus Local State Logical Relations Game Semantics Environmental Bisimulations 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nikos Tzevelekos 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.10351.5 urn:nbn:de:0030-drops-28092 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.5 eng https://creativecommons.org/licenses/by/4.0/legalcode