In January 2010, Martin Churchill (a PhD student at the Universi= ty 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 so= me of Martin's recent work in the proof assistant (and dependently-typed fu= nctional programming language) Agda.

=20The recent work in question concerns a *Logic of Sequentiality* a=
nd its related semantics. It is well-known that game semantics is well suit=
ed to modelling higher-order imperative programs. Thus, one may give semant=
ics 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 re=
present (finite) games, and proofs represent (total) strategies on these ga=
mes. Further, this system has a set of core rules satisfying the property t=
hat 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 (

A general aim of this work is as follows:

=20- =20
- Formalise this proof system =20
- Formalise some game semantics, and the semantics of proofs as strategie= s =20
- Provide an environment for "running" a given strategy, where the user e= nters the environment-moves and the system responds according to that strat= egy =20

In the two-weeks of Martin's visit at AIST, a sucessful start to this ha= s occurred. We have so far:

=20- =20
- Formalised game semantics in Agda (including games, strategies, mediati= ng copycat strategies, composition...) =20
- Formalised the system WS from A Logic of Sequentiality =20
- Formulated a "semantic function" taking a proof to its corresponding st= rategy for WS =20
- Provided a notion of Annotated Game, allowing textual data to be added = to moves for purposes of "running" them =20
- Implemented this in the case of the semantics of WS, where a move is an= notated with the formula representing the "rest of the game" to be played=20
- Provided the ability to print out (annotated) games as a tree =20
- Provided an environment to "run" strategies on annotated games, as desc= ribed above. =20

Additional achievements include:

=20- =20
- Formalising the cut elimination procedure of core-WS (but not completed= its soundness proof) =20
- Encoding part of the full completeness theorem (extracting a proof from= a strategy) =20

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 Apri= l will be a useful opportunity to do this. Further continuations include fo= rmalising proofs about WS in Agda (such as full completeness and soundness = of cut).

=20In addition, Martin spoke with other researchers in AIST about their res= earch interests, and this will continue in March/April as a number of these= researchers visit Bath.

=20A snapshot of this work can be found at http://people.b= ath.ac.uk/mdc25/AgdaWS

=20**Postscript (16.09.10)**

In further collaborations between Martin, Makoto and others, we have now= also done the following:

=20- =20
- Formalised a finitary imperative language and its embedding into WS (he= nce this gives a way to calculate the concrete strategy, and core proof, as= sociated by a program) =20
- Restructured the full completeness procedure to also contain its termin= ation proof, and hence pass Agda's termination checker. =20
- Explored the feasibility of formalising infinite games and partial stra= tegies in Agda, and completed this to the extent to this is practical in th= e current version of Agda. This was done at the twelfth Agda Implementors Meeting =20