eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-04
10351
1
16
10.4230/DagSemProc.10351.1
article
10351 Abstracts Collection – Modelling, Controlling and Reasoning About State
Ahmed, Amal
Benton, Nick
Birkedal, Lars
Hofmann, Martin
From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351
``Modelling, Controlling and Reasoning About State '' was held in
Schloss Dagstuhl~--~Leibniz Center for Informatics. During the
seminar, several participants presented their current research, and
ongoing work and open problems were discussed. Abstracts of the
presentations given during the seminar as well as abstracts of seminar
results and ideas are put together in this paper. Links to extended
abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10351/DagSemProc.10351.1/DagSemProc.10351.1.pdf
Mutable State
Program Logics
Semantics
Type Systems
Verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-04
10351
1
4
10.4230/DagSemProc.10351.2
article
10351 Executive Summary – Modelling, Controlling and Reasoning About State
Ahmed, Amal
Benton, Nick
Birkedal, Lars
Hofmann, Martin
From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351
``Modelling, Controlling and Reasoning About State ''
was held in Schloss Dagstuhl~--~Leibniz Center for
Informatics. 44 researchers, with interests and expertise in many
different aspects of modelling and reasoning about mutable state, met
to present their current work and discuss ongoing projects and open
problems. This executive summary provides a general overview of the goals of the
seminar and of the topics discussed.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10351/DagSemProc.10351.2/DagSemProc.10351.2.pdf
Mutable State
Program Logics
Semantics
Type Systems
Verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-04
10351
1
12
10.4230/DagSemProc.10351.3
article
A Theory of Termination via Indirection
Dockins, Robert
Hobor, Aquinas
Step-indexed models provide approximations to a class of domain
equations and can prove type safety, partial correctness, and program
equivalence; however, a common misconception is that they
are inapplicable to liveness problems. We disprove this by applying
step-indexing to develop the first Hoare logic of total correctness
for a language with function pointers and semantic assertions.
In fact, from a liveness perspective, our logic is stronger: we verify
explicit time resource bounds. We apply our logic to examples containing
nontrivial "higher-order" uses of function pointers and we
prove soundness with respect to a standard operational semantics.
Our core technique is very compact and may be applicable to other
liveness problems. Our results are machine checked in Coq.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10351/DagSemProc.10351.3/DagSemProc.10351.3.pdf
Step-indexed Models
Termination
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-04
10351
1
9
10.4230/DagSemProc.10351.4
article
Limitations of Applicative Bisimulation (Preliminary Report)
Koutavas, Vasileios
Levy, Paul Blain
Sumii, Eijiro
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.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10351/DagSemProc.10351.4/DagSemProc.10351.4.pdf
Imperative languages
higher-order functions
local state
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-04
10351
1
18
10.4230/DagSemProc.10351.5
article
Program Equivalence with Names
Tzevelekos, Nikos
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.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10351/DagSemProc.10351.5/DagSemProc.10351.5.pdf
Nu-calculus
Local State
Logical Relations
Game Semantics
Environmental Bisimulations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-04
10351
1
10
10.4230/DagSemProc.10351.6
article
Step-Indexed Biorthogonality: a Tutorial Example
Pitts, Andrew M.
The purpose of this note is to illustrate the use of step-indexing combined with biorthogonality to construct syntactical logical relations. It walks through the details of a syntactically simple, yet non-trivial example: a proof of the "CIU Theorem'' for contextual equivalence in the untyped call-by-value $lambda$-calculus with recursively defined functions.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10351/DagSemProc.10351.6/DagSemProc.10351.6.pdf
Biorthogonality
logical relations
operational semantics
step-indexing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-04
10351
1
9
10.4230/DagSemProc.10351.7
article
Step-Indexing: The Good, the Bad and the Ugly
Benton, Nick
Hur, Chung-Kil
Over the last decade, step-indices have been widely used for the
construction of operationally-based logical relations in the presence
of various kinds of recursion. We first give an argument that
step-indices, or something like them, seem to be required for defining
realizability relations between high-level source languages and
low-level targets, in the case that the low-level allows egregiously
intensional operations such as reflection or comparison of code
pointers. We then show how, much to our annoyance, step-indices also
seem to prevent us from exploiting such operations as aggressively as
we would like in proving program transformations.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10351/DagSemProc.10351.7/DagSemProc.10351.7.pdf
Step-Indexing
Logical Relations
Low-Level Languages
Compiler Correctness