Child pages
  • 15th Wessex Theory Seminar

Versions Compared


  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Migrated to Confluence 4.0


We present a full classification of decidable and undecidable cases
for contextual equivalence in a finitary ML-like language equipped
with full ground storage (both integers and reference names can be
stored). The simplest undecidable type is unit -> unit -> unit. At the
technical level, our results marry game semantics with
automata-theoretic techniques developed to handle infinite
alphabets. On the automata-theoretic front, we show decidability of
the emptiness problem for register pushdown automata extended with
fresh-symbol generation.


From Bath:

  • Catrin Campbell-Moore
  • Anupam Das
  • Jim Laird
  • Alvin Šipraga

From Birmingham:

  • Félix Baschenis
  • Ian Batten
  • Sergiu Bursuc
  • Liang-Ting Chen
  • Martín Escardó
  • Bertfried Fauser
  • Olle Fredriksson
  • Dan Ghica
  • Achim Jung
  • Paul Blain Levy
  • Uday Reddy
  • Asiri Rathnayake
  • Umberto Rivieccio
  • Maxim Strygin
  • Hayo Thielecke
  • Steve Vickers
  • Chuangjie Xu

From Leicester:

  • Andrzej Murawski

From London:

  • Björn Lellmann (Imperial)
  • Dusko Pavlovic (Royal Holloway)
  • Nobuko Yoshida (Imperial)

From Nottingham:

  • Philippa Cowderoy

From Southampton:

  • Julian Rathke
  • Owen Stephens

From Sussex:

  • Martin Berger
  • Bernhard Reus

See all Wessex sites involved and meetings so far.