The second exchange of the project consisted of a visit to AIST, Osaka by two PhD students in the department of Computer Science - Ana Carolina Martins Abbud and Martin Churchill. This visit began on 18th May, 2009.
The main aim of this short trip was to establish further links between the work of Bath and AIST, and in particular explore ideas that could be used as the foundation of a longer visit between the visitors and AIST in future.
A total of four talks were given, presented by the visitors from the University of Bath. Some of the talks were given at the University of Kyoto as part of a visit to this location by the visitors and a number of AIST researchers (see below.)
In addition, the visitors talked to AIST researchers about their interests, following the various talks given on such matters at the University of Bath. In particular they had extended discussions with Hitoshi Ohsaki, Makoto Takeyama and Shunsuke Yatabe.
In the former case, a discussion occurred regarding Hitoshi's work on Tree Automata, and its relation to the more algorithmic aspects of game semantics. In particular, there may be a link here as Hitoshi's Tree Automata are machines for expressing tree languages, and games (and strategies) are special kinds of trees. In particular some recent work of Martin directly deals with sets of trees, and such a set may or may not be recognisable by various forms of tree automata.
The visitors also talked to Makoto Takeyama and Shunsuke Yatabe about their work - in particular some helpful suggestions were made regarding the work of Ana and the functor from the category of games into coherence spaces. The visitors share many research interests with Shunsuke Yatabe (linear logic, game semantics etc) and they look forward to further interaction on Shunsuke's month-long visit to Bath in the autumn.
In addition, Makoto Takeyama gave a talk on the theorem prover Agda and in particular went through an extended example to show how it could be used. Ana and Martin had seen Agda before and have been impressed by it, but this was a good opportunity to get some hands-on experience with the guidance of an expert.
As a result of the talk from Makoto Takeyama about Agda, it was clear that the contents of Martin's talk Proofs and Polarised Games would both be well-suited to and would benefit from formalisation in Agda. This inspired him to spend a couple of days working on this. As far as we know this is the first formalisation of game semantics in such a dependently typed language, although some work of John Longley relates to implementing game semantics in ML. It is suited to the content of Martin's talk and in particular it's possible that the full completeness result described herein could be formalised in Agda. In addition, this work allowed Martin Churchill to rapidly learn the subtleties of Agda far faster than would have been possible if he were to do so without an expert at hand. Some of the initial resulting code - formalising the definitions and semantics given in the talk - may soon be available.
As part of the visit, Ana and Martin went to Kyoto University with AIST researchers. Many researchers at RIMS have worked at AIST, and many of these researchers share interest with the visitors. Martin and Ana presented talks here, and had valuable discussions with researchers of Kyoto University such as Prof. Kazushige Terui and Ichiro Hasuo.
We feel that the visit was a success, and provided the opportunity for various valuable discussions. Prospects of a future visit of Martin and Ana to AIST look good, and we look forward to further interactions.