**11th Wessex Theory Seminar**

The eleventh meeting of the Wessex Theory Seminar will take place on Friday 17th June 2011 at the University of Leicester.

It takes 10-15 minutes to reach the campus from the train station on foot.

The talks will take place in the Attenborough Building in LT3 (seminar block on the map).

**Preliminary Programme**

**1pm Lunch** (Campus, Charles Wilson Building, 5th floor)

**2-6pm Talks**

**2:00-2:30**Martin Churchill (Bath): Imperative Programs as Proofs via Game Semantics

**2:30-3:30**Pierre Clairambault (Bath): Isomorphisms of types in the presence of higher-order references

**3:30-4:00**coffee break (Library Cafe)

**4:00-4:30**David Hopkins (Oxford): A Fragment of ML Decidable by Visibly Pushdown Automata

**4:30-5:10**Paul Levy (Birmingham): Operational Game Semantics

**afterwards** Pub Drinks & Dinner at Kayal*

**Abstracts**

Martin Churchill, **Imperative Programs as Proofs via Game Semantics**

Game semantics extends the Curry-Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. We can embed intuitionistic first-order linear logic into this system, as well as an imperative total programming language. The logic makes explicit use of the fact that in the game semantics the exponential can be expressed as a final coalgebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof.

Pierre Clairambault, **Isomorphisms of types in the presence of higher-order references**

We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterising isomorphisms of types in a finitary language L_2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L_2 with natural numbers.

David Hopkins, **A Fragment of ML Decidable by Visibly Pushdown Automata**

We consider the problem of determining whether two terms of an ML-like language are observationally equivalent. RML is a simply-typed, call-by-value language which may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct. In general, observational equivalence for RML is an undecidable problem. However, by restricting the types allowed we obtain a decidability result. By a short type, we mean a type of order at most 2 and arity at most 1. We consider the fragment of (finitary) RML, RML_OStr, consisting of terms-in-context such that (1) the term has a short type, and (2) every argument type of the type of each free variable is short. RML_OStr is surprisingly expressive; it includes several instances of (in)equivalence in the literature that are challenging to prove using methods based on logical relations. Using the fully abstract game semantics of RML, we reduce the problem of observational equivalence for RML_OStr terms to the decidable problem of language equivalence of visibly pushdown automata. When restricted to terms in canonical form, the problem is EXPTIME-complete.

Paul Levy, **Operational game semantics**

Abramsky, Honda and McCusker gave a denotational semantics for a higher-order language with general references, i.e. not only stored integers but stored functions too. Their semantics uses games and strategies with justification pointers, in the manner of Hyland and Ong. In this talk we give an account of this model from an operational perspective. Thus compositionality becomes a theorem rather than a definition. This is joint work with Jim Laird and Soren Lassen.

**Attendance**

From Bath:

- Martin Churchill
- Pierre Clairambault
- Anupam Das

From Birmingham:

- Liang-Ting Chen
- Olaf Klinke
- Paul Levy

From Leicester:

- Artur Boronat
- Roy Crole
- Alexander Kurz
- Tadeusz Litak
- Andrzej Murawski
- Fer-Jan de Vries

From Nottingham:

- Thorsten Altenkirch

From Oxford:

- David Hopkins

From Swansea:

- Ulrich Berger

See all Wessex sites involved and meetings so far.