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:
- Formalise this proof system
- Formalise some game semantics, and the semantics of proofs as strategies
- Provide an environment for "running" a given strategy, where the user enters the environment-moves and the system responds according to that strategy
In the two-weeks of Martin's visit at AIST, a sucessful start to this has occurred. We have so far:
- Formalised game semantics in Agda (including games, strategies, mediating copycat strategies, composition...)
- Formalised the system WS from A Logic of Sequentiality
- Formulated a "semantic function" taking a proof to its corresponding strategy for WS
- Provided a notion of Annotated Game, allowing textual data to be added to moves for purposes of "running" them
- Implemented this in the case of the semantics of WS, where a move is annotated with the formula representing the "rest of the game" to be played
- Provided the ability to print out (annotated) games as a tree
- Provided an environment to "run" strategies on annotated games, as described above.
Additional achievements include:
- Formalising the cut elimination procedure of core-WS (but not completed its soundness proof)
- Encoding part of the full completeness theorem (extracting a proof from a strategy)
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:
- Formalised a finitary imperative language and its embedding into WS (hence this gives a way to calculate the concrete strategy, and core proof, associated by a program)
- Restructured the full completeness procedure to also contain its termination proof, and hence pass Agda's termination checker.
- Explored the feasibility of formalising infinite games and partial strategies in Agda, and completed this to the extent to this is practical in the current version of Agda. This was done at the twelfth Agda Implementors Meeting