The first extended exchange on the project was John Power's visit to AIST, departing Bath on 3 December. Taking into account travel time, recovery from travel, and holidays, it was efffectively a three week visit.
The main aim of the exchange was for Bath to acquire a current understanding of the relevant activity of CVS and to see, in some detail, likely points 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 Dependability.
There are currently four projects at CVS that seem likely contact points with Bath. They are as follows:
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
- to establish a standard for dependable systems
- to provide conformance evaluation guidelines
- to provide development guidelines.
Logical analysis is to be used in order to provide the guidelines, and relevant topics are dependability, formal methods, and natural language processing.
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 workshop in September. Its aims are
- to fix a format for specifications
- to provide a consistency checker for specifications.
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 expected to start and end with Japanese language statements.
The remaining two projects involve collaboration with specific industrial companies which cannot be named. So privacy and copyright issues apply to these.
Railway Fare Calculation System
This is led at CVS by Hitoshi Ohsaki. It originally used a SAT solver, which 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.
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.
These four projects would be natural projects for visitors from Bath to AIST to study, perhaps including limited involvement. The use of a SAT solver and its limitations could conceivably be of interest to the Logic Programming group in Bath.
In addition to the four above-mentioned projects, there are other more individual contacts that have potential. A few that look particularly positive are as follows:
- Takahashi Kitamura recently finished a PhD in Beijing with Lin Huimin, who is a former student of Matthew Hennessy. Kitamura-san has specific interest in the modal mu-calculus, which in turn can be modelled by game semantics, 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 homepage). Kitamura-san himself does not currently know game semantics, but it is a speciality at Bath, so that may be a point of contact.
- 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.
- 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 game semantics to his work, which was inspired by a language developed at MIT.
For the opposite direction, i.e., in regard to explaining Bath work to the AIST group, John gave a talk on structural operational semantics for computational effects at AIST on Thursday 18 December, based on a paper published 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 direct, explicit relevance to the specific research theme of the Bath-AIST project 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 December. A number of researchers at RIMS have worked at AIST, so the visit formed a natural part of the Bath-AIST relationship. In Kyoto, he worked with Prof Masahito Hasegawa (Hassei), who had been his PhD student in Edinburgh, with Shinya Katsumata, who had also been an Edinburgh PhD student, Craig Pistore, a former PhD student of Ross Street at Macquarie University in Sydney, Australia, and with two Japanese post-graduate students of Hassei. The bulk 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 theory.
Ichiro 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 currently separate from its link with the Mathematical Foundations group at the University of Bath. The link is with Martyn Thomas, a founder of Praxis, who might be a natural person to invite to join the interaction if the rules allow for that.