In January 2010, Martin Churchill (a PhD student at the University of Bath) made a second visit to the CVS site in Osaka. The main purpose of this trip was to continue working with Makoto Takeyama on formalising some of Martin's recent work in the proof assistant (and dependently-typed functional programming language) Agda.
The recent work in question concerns a Logic of Sequentiality and its related semantics. It is well-known that game semantics is well suited to modelling higher-order imperative programs. Thus, one may give semantics of a higher-order imperative program as a strategy on a game. Logic of Sequentiality attempts to give a logical characterisation of these strategies. In particular, it provides a proof system WS where formulas represent (finite) games, and proofs represent (total) strategies on these games. Further, this system has a set of core rules satisfying the property that proofs of a given formula using only these core rules are in one-to-one correspondance with total strategies on the denotation of that formula (full completeness).
A general aim of this work is as follows:
In the two-weeks of Martin's visit at AIST, a sucessful start to this has occurred. We have so far:
Additional achievements include:
On February 2nd, Martin presented a talk entitled Game Semantics and Agda at the Osaka Software Engineering Workshop at CVS.
There are some ends that need tying up, and Takeyama-san's visit in April will be a useful opportunity to do this. Further continuations include formalising proofs about WS in Agda (such as full completeness and soundness of cut).
In addition, Martin spoke with other researchers in AIST about their research interests, and this will continue in March/April as a number of these researchers visit Bath.
A snapshot of this work can be found at http://people.bath.ac.uk/mdc25/AgdaWS
In further collaborations between Martin, Makoto and others, we have now also done the following: