Dagstuhl Seminar 10351
Modelling, Controlling and Reasoning About State
( Aug 29 – Sep 03, 2010 )
- Amal Ahmed (Indiana University - Bloomington, US)
- Nick Benton (Microsoft Research UK - Cambridge, GB)
- Lars Birkedal (IT University of Copenhagen, DK)
- Martin Hofmann (LMU München, DE)
- Annette Beyer (for administrative matters)
The combination of dynamically allocated, mutable data structures and higher-order features is present in almost all programming languages, from C to ML, Java and C#. The search for good models and reasoning principles for, and language features that tame the complexity of, this combination goes back many decades. Recent years have seen a number of significant advances in our semantic understanding of state and encapsulation, including the development of separation logic, substructural type systems, models using parametric and step-indexed logical relations, and new bisimulation-based reasoning methods.
At the same time, concern about reliability, correctness and security of software has led to increased interest in tool and language support for specification and verification of realistic languages (for example JML and Spec#), certified and certifying compilation, proof-carrying code, safe systems programming languages (such as Cyclone and CCured), and practical type systems capturing and controlling subtle aspects of state, such as ownership, effects, information flow and protocol conformance. Formalizing the meaning and the soundness of these new languages, analyses and type systems is a major motivation for the development of the theory described above.
This is an exciting and important research area. Mathematically sound reasoning principles for state, combined with recent advances in program analysis and machine-assisted proof, have the potential to lead to improved programming languages, compilers, verification technology and even to new approaches to software deployment and operating system design.
This seminar built on the success of Dagstuhl Seminar 08061 `Types, Logics and Semantics for State', held in February 2008, though with slightly less emphasis on bringing together researchers from very different communities, and slightly more on in-depth technical discussion and collaboration on key technical issues such as the correct modelling of independence, recursive store, step-indexing and purity.
Among the research challenges addressed at the workshop were:
- What are the semantic foundations of existing logics and type systems for ownership, confinement, effects and permissions, and how may such foundations be used not only to understand and improve these systems, but also to relate them formally to one another?
- How can we reason about controlled use of state at multiple levels of abstraction, for example in relating high-level, language-enforced restrictions to low-level guarantees on the behaviour of compiled code?
- What is the right mix of approaches to the control of state and other effects, both in low-level languages and in modern high-level languages with higher-order features? How to balance language design and type systems, automated verification tools and machine assisted proof?
- What is the relationship between the recently appeared step-indexing method for establishing soundness of type systems and fully denotational approaches? In particular, how can denotational methods for mixed-variance equations for predicates and relations be transferred to step-indexed models of types, and how can the respective soundness properties, which are in general not logically equivalent, be compared?
- How can we quantify and use the additional information gained by modular analyses that do not require knowledge of the whole program? Is observational equivalence really the ultimate equivalence?
- How should we deal with the mixed-variance equations for predicates and relations that appear in the denotational modelling of storable procedures (``higher-order store''). In recent developments we have seen such equations that were solvable in an ad-hoc way but escaped the established solution theory.
- How can the algebraic approach developed for global state via Lawvere theories be extended to local state?
This was an intense and productive week. With a relatively large number of particpants, most of whom wanted to speak, the schedule was relatively tight; though we did this time manage to incorporate the traditional hiking excursion on Wednesday afternoon. Discussions continued late into the night throughout the week, and were still unbelievably technical even at 2am! The proceedings contain five papers on techniques, all of which were inspired or influenced by discussions at the seminar.
- Amal Ahmed (Indiana University - Bloomington, US) [dblp]
- Robert Atkey (University of Strathclyde, GB) [dblp]
- Nick Benton (Microsoft Research UK - Cambridge, GB) [dblp]
- Lennart Beringer (Princeton University, US) [dblp]
- Lars Birkedal (IT University of Copenhagen, DK) [dblp]
- Brian Campbell (University of Edinburgh, GB)
- Arthur Chargueraud (INRIA - Le Chesnay, FR)
- Adam Chlipala (Harvard University - Cambridge, US) [dblp]
- Robert Dockins (Princeton University, US)
- Derek Dreyer (MPI-SWS - Saarbrücken, DE) [dblp]
- Philippa Gardner (Imperial College London, GB) [dblp]
- Aquinas Hobor (National University of Singapore, SG) [dblp]
- Martin Hofmann (LMU München, DE) [dblp]
- Chung-Kil Hur (University Paris-Diderot, FR) [dblp]
- Steffen Jost (University of St. Andrews, GB) [dblp]
- Andrew Kennedy (Microsoft Research UK - Cambridge, GB) [dblp]
- Vasileios Koutavas (Trinity College Dublin, IE) [dblp]
- Neel Krishnaswami (Microsoft Research UK - Cambridge, GB) [dblp]
- Paul Blain Levy (University of Birmingham, GB) [dblp]
- Paul-Andre Mellies (University Paris-Diderot, FR) [dblp]
- Rasmus Ejlers Mogelberg (IT University of Copenhagen, DK) [dblp]
- Andrzej Murawski (University of Oxford, GB) [dblp]
- Aleksandar Nanevski (Technical University of Madrid, ES) [dblp]
- Georg Neis (MPI-SWS - Saarbrücken, DE)
- Chih-Hao Luke Ong (University of Oxford, GB) [dblp]
- Andrew M. Pitts (University of Cambridge, GB) [dblp]
- Francois Pottier (INRIA - Le Chesnay, FR) [dblp]
- Uday Reddy (University of Birmingham, GB)
- Bernhard Reus (University of Sussex - Brighton, GB)
- Noam Rinetzky (Queen Mary University of London, GB) [dblp]
- Dulma Rodriguez (LMU München, DE)
- Andreas Rossberg (MPI-SWS - Saarbrücken, DE) [dblp]
- Jan Schwinghammer (Universität des Saarlandes, DE)
- Zhong Shao (Yale University, US) [dblp]
- Ian Stark (University of Edinburgh, GB) [dblp]
- Sam Staton (University of Cambridge, GB) [dblp]
- Eijiro Sumii (Tohoku University - Sendai, JP) [dblp]
- Kasper Svendsen (IT University of Copenhagen, DK) [dblp]
- Nicolas Tabareau (Ecole des Mines de Nantes, FR) [dblp]
- Jacob Thamsborg (IT University of Copenhagen, DK)
- Hayo Thielecke (University of Birmingham, GB)
- Nikos Tzevelekos (University of Oxford, GB) [dblp]
- David Walker (Princeton University, US) [dblp]
- Hongseok Yang (Queen Mary University of London, GB) [dblp]
- Dagstuhl Seminar 08061: Types, Logics and Semantics for State (2008-02-03 - 2008-02-08) (Details)
- Programming Languages / Compiers
- Semantics / Formal Methods
- Verification / Logic
- mutable state
- type systems
- program logics