Child pages
  • 11th Wessex Theory Seminar
Skip to end of metadata
Go to start of metadata

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 53 Next »

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.

Leicester map
Campus map

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

Preliminary Programme


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

2-6pm Talks (offers still welcome)

  • David Hopkins (Oxford): A Fragment of ML Decidable by Visibly Pushdown Automata
  • Martin Churchill (Bath): Imperative Programs as Proofs via Game Semantics

after 6pm Pub Drinks & Dinner at Kayal*

Abstracts


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.


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

From Birmingham:

  • Paul Levy

From Cambridge:

From Imperial:

From Leicester:

  • Alexander Kurz
  • Andrzej Murawski

From Oxford:

  • David Hopkins

From Queen Mary:

From Southampton:

From Sussex:

From Swansea:

See all Wessex sites involved and meetings so far.

  • No labels