IT University of Copenhagen, Denmark
4pm Monday 1st September 2008
Room 4.31, Informatics Forum
Note nonstandard day
Most programming languages contain a construction for declaring local state, i.e., variables that can only be accessed by a specified piece of the program. This restriction of access provides an important information hiding principle: the behaviour of a program should be independent of the concrete implementation and use of local state. Relational reasoning has proved useful for formalising this idea: if two programs are implemented using local state, and we can show that there exists a relation between the local states preserved by the programs, then the programs should be contextually equivalent.
In this talk I present a type theory for computations with ground local state and a model of it constructed using nominal sets. I then show how relational reasoning can be modeled by constructing a very similar model using relations on nominal sets. Compared to earlier work, this model simplifies the relational reasoning because we can use the techniques of nominal sets to get rid of the Kripke style constructions in the definition of the relations.
In examples I will show how a relational variant of the type theory can be used to show contextual equivalence of programs, and I will discuss how the operation allocating local state can be seen as relationally parametric in the type of the allocated state.