The first extended exchange on the project was John Power's firs= t visit to AIST, departing Bath on 3 December 2008. Taking into account tra= vel time, recovery from travel, and holidays, it was efffectively a three w= eek visit.

=20The main aim of the exchange was for Bath to acquire a current understan= ding of the relevant activity of CVS and to see, in some detail, likely poi= nts of contact between the Mathematical Foundations group at Bath and CVS. = The most notable change at CVS since John's previous visit, two years ago, = was the start, just two months ago, of a 5.5 year CREST-funded project on D= ependability.

=20There are currently four projects at CVS that seem likely contact points= with Bath. They are as follows:

=20**Dependability**

As mentioned above, this is a 5.5 year project funded by CREST (which is= roughly equivalent to the UK's EPSRC) led by Yoshiki Kinoshita and Makoto = Takeyama. Its aims are

=20- =20
- to establish a standard for dependable systems =20

- =20
- to provide conformance evaluation guidelines =20

- =20
- to provide development guidelines. =20

Logical analysis is to be used in order to provide the guidelines, and r= elevant topics are dependability, formal methods, and natural language proc= essing.

=20**Specification of Embedded Systems**

This project is funded by METI and is joint work with CSK. It is led at = CVS by Yatabe-san, who gave a talk about it at the second Bath-AIST worksho= p in September. Its aims are

=20- =20
- to fix a format for specifications =20

- =20
- to provide a consistency checker for specifications. =20

For the second aim, "consistency" is to be understood in the broad sense= of the word rather than in its narrowly defined logical sense. The plan is= to use Agda for the consistency checker, but users of the system are expec= ted to start and end with Japanese language statements.

=20The remaining two projects involve collaboration with specific industria= l companies which cannot be named. So privacy and copyright issues apply to= these.

=20**Railway Fare Calculation System**

This is led at CVS by Hitoshi Ohsaki. It originally used a SAT solver, w= hich resolved an internal problem, to the considerable satisfaction of the = project organisers. But as the SAT solver is limited, the idea is to extend= the system using Agda.

=20**Improvement of a Software Development Process**

This is led at CVS by Kato-san, with whom John has had less interaction = to date than with the previously mentioned researchers. It is joint with a = specific automobile software company.

=20These four projects would be natural projects for visitors from Bath to = AIST to study, perhaps including limited involvement. The use of a SAT solv= er and its limitations could conceivably be of interest to the Logic Progra= mming group in Bath.

=20In addition to the four above-mentioned projects, there are other more i= ndividual contacts that have potential. A few that look particularly positi= ve are as follows:

=20- =20
- Takahashi Kitamura recently finished a PhD in Beijing with Lin Huimin, =
who is a former student of Matthew Hennessy. Kitamura-san has specific inte=
rest in the modal mu-calculus, which in turn can be modelled by game semant=
ics, with the games models being of interest to specialists in the modal mu=
-calculus, such as Prof Colin Stirling in Edinburgh (see the slides on
*= Higher-order matching, games and automata*on Colin's homep= age). Kitamura-san himself does not currently know game semantics, but = it is a speciality at Bath, so that may be a point of contact. =20

- =20
- Yoriyuki Yamagata is currently away from AIST, visiting Stefano Berardi= in Turin, Italy. But apparently he has specific interest in game semantics= . So he too might be a natural contact for the Bath group at AIST. He also = collaborates with Susumu Hayashi. =20

- =20
- a recent visitor to AIST, but working at Nagoya University, was Tetsuo = Yamanaka, who is working on "reversible computation". The PMI project only = funds Bath-AIST interactions, but Yamanaka-san used structural operational = semantics, and one wonders whether there may be a sensible application of g= ame semantics to his work, which was inspired by a language developed at MI= T. =20

For the opposite direction, i.e., in regard to explaining Bath work to t=
he AIST group, John gave a talk on structural operational semantics for com=
putational effects at AIST on Thursday 18 December, based on a paper publis=
hed by ENTCS this year, *Tensors of Comodels and Models for Operational =
Semantics* (MFPS 2008 paper). Although that specific work=
is joint with Gordon Plotkin in Edinburgh, the techniques used are of dire=
ct, explicit relevance to the specific research theme of the Bath-AIST proj=
ect as stated. So the talk is of immediate relevance to the project.

He also made a side visit to Kyoto University's RIMS on Monday 15 Decemb= er. A number of researchers at RIMS have worked at AIST, so the visit forme= d a natural part of the Bath-AIST relationship. In Kyoto, he worked with Pr= of Masahito Hasegawa (Hassei), who had been his PhD student in Edinburgh, w= ith Shinya Katsumata, who had also been an Edinburgh PhD student, Craig Pis= tore, a former PhD student of Ross Street at Macquarie University in Sydney= , Australia, and with two Japanese post-graduate students of Hassei. The bu= lk of the day amounted to giving a version of the talk he was soon to give = at AIST, as well as answering some technical questions about category theor= y.

=20Ichiro Hasuo, one of the RIMS researchers, was unwell on 15 December, so=
he visited AIST on Friday 19 December for research discussions. He worked =
at AIST some time earlier. He has worked for some time on the *microcosm=
principle*, but John suggested earlier in the year that a considerably=
more interesting question is that of expressiveness, which Ichiro has now =
begun to address. So there was substantial discussion about expressiveness =
for *discrete Lawvere 2-theories*, ideas from which may well benefit=
the research funded here.

One final side remark is that AIST has a link with Bath that is currentl= y separate from its link with the Mathematical Foundations group at the Uni= versity of Bath. The link is with Martyn Thomas, a founder of Praxis, who m= ight be a natural person to invite to join the interaction if the rules all= ow for that.

=20**Future work arising from the visit**

The specific plans to extend the interactions generated by this visit ar= e for an AIST group to visit Bath for a third Bath-AIST workshop, for Yatab= e-san and Kitamura-san to make extended visits to Bath to explore the above= ideas, for Jim Laird to visit AIST, hosted by Yamagata-san, and for Yoshik= i Kinoshita perhaps to make an extended visit to Bath to check the potentia= l for a permanent relationship beyond the grant period.