Games for Logic and Programming Languages

Inaugural edition: Etaps 2005, Edinburgh, 2-3 April 2005


News

There will be a special issue in the Annals of Pure and Applied Logic. Submission is open, but all workshop participants are encouraged to submit. The deadline is November 1st, 2005.

Introduction

In the past decade game semantics has emerged as a new and successful paradigm in the field of semantics of logics and programming languages.  Game semantics made its breakthrough in computer science in the early 90s, providing an innovative set of methods and techniques for the analysis of logical systems. Subsequently, game-semantic techniques led to the development of the first syntax-independent fully-abstract models for a variety of programming languages, ranging from the purely functional to languages with non-functional features such as control, references or concurrency.  There are also emerging connections between game semantics and other semantic theories, notably theories of concurrency such as the pi-calculus, and traditional tree-based semantics of lambda calculi. In addition to semantic analysis, an algorithmic approach to game semantics has recently been developed, with a view to applications in computer assisted verification and program analysis.

The aim of the workshop is to provide opportunity for interaction with other Etaps'05 events and to become a major meeting point in the research area of Game Semantics and its applications.

Workshop Program

Day 1: Saturday, April 2nd

  • 09:30 Luke Ong (Oxford), Classifying Decidable fragments of Idealized Algol (invited talk)
  • 10:30 Coffee break
  • 11:00 Interaction Systems
    • P. Hyvernat (Luminy), Synchronous games, simulations and lambda-calculus
    • J. Aguado and M. Mendler (Bamberg), Constructive semantics for instantaneous reactions
    • J. Laird (Sussex), A game semantics of the asynchronous pi-calculus and its dual
  • 14:00 Theoretical aspects
    • R. Harmer (Paris 7), Affine strategies in arena games
    • M. Hirschowitz (Paris 7), Abstract games
    • A. Schalk (Manchester), Concrete data structures as games
  • 15:30 Coffee break
  • 16:00 Proof search
    • P. Rondogiannis (Athens) and W. Wadge (Victoria), An infinite-game semantics for negation in logic programming
    • D. Miller and A. Saurin (INRIA), A game semantics for proof search: preliminary results
    • D. Pym (Bath) and E. Ritter (Birmingham), A games semantics for reductive logic and proof-search
  • 17:30 End of session

Day 2: Sunday, April 3rd

  • 9:30 Luca de Alfaro (UCSC), Real-time component interfaces (invited talk)
  • 10:30 Coffee break
  • 11:00 Model checking
    • A. Murawski (Oxford), Functions with local state: from regularity to undecidability
    • A. Dimovski (Warwick), D. R. Ghica (Birmingham) and R. Lazic (Warwick), Abstraction-refinement for game-based model checking
    • A. Morgenstern and K. Schneider (Kaiserslautern), A unified model checking framework for the supervisor synthesis problem
  • 14:00 Programming language semantics
    • G. McCusker and M. Wall (Sussex), Categorical and game semantics for SCIR
    • B. Leperchey (Paris 7), Time and games
    • P. B. Levy (Birmingham), Infinite trace equivalence
  • 15:30 Coffee break
  • 16:00 Information flow
    • S. Berardi (Turin), T. Coquand (Chalmers) and S. Hayashi (Kobe), Games with 1-backtracking
    • Y. Delbecque (MgGill), Information and information flow in game semantics
    • J. Juerjens (Munich), Towards using game semantics for crypto protocol verification: Lorenzen games
  • 17:30 End of session

Publication

This is intended to be an informal workshop. Participants are encouraged to present work in progress, overviews of more extensive work, and programmatic/position papers, as well as completed projects. We therefore ask for submission both of short abstracts outlining what will be presented at the workshop and of longer papers describing completed work, either published or unpublished, in the following areas:

  • Game theory and interaction models in semantics
  • Games-based design and verification
  • Logics for games and games for logics
  • Algorithmic aspects of games

A participants' proceedings will be distributed at the workshop and made available as a Oxford University technical report. A special journal issue associated with the workshop is being considered; this will be discussed at the workshop.

games

Important dates

November 1st: APAL submission

Steering committee

  • Samson Abramsky, Oxford University
  • Pierre-Louis Curien, Universite Paris 7
  • Dan Ghica, University of Birmingham
  • Russ Harmer, Universite Paris 7
  • Kohei Honda, Queen Mary University of London
  • Furio Honsell, University of Udine
  • Martin Hyland, Cambridge University (Chair)
  • Radha Jagadeesan, DePaul University
  • Jim Laird, University of Sussex
  • Guy McCusker, University of Sussex
  • Luke Ong, Oxford University
  • Andrea Schalk, University of Manchester
  • Thomas Streicher, Universitaet Darmstadt