**Wessex Theory Seminar, 14 Apr.**

I gave a talk with the title *Hoare in Agda.* I encoded or implemented Hoare Logic in Agda with Makoto Takeyama. My talk is about design decisions I made during this work. Slides are included as Appendix A in this report.

**Seminar at Swansea, 15 Apr.** This is the same talk as one given in Wessex Theory Seminar.

**Seminar at City University, London, 21 Apr.** I gave two talks. One is an overview of dependability study being done around our group in AIST in the past and coming year; its slides are included as Appendex B with the title Introduction to Dependability Research at AIST in this report. Another talk is about a structure of unit of assurance case; we set up a notion of unit between the level of nodes of those graphical notations such as GSN and CAE and the level of the whole Assurance Case. Its slides with the title Argument Units of Assurance Cases and their Interpretation is included in this report as Appendex C.

List of Talks in Wessex Theory Seminar, 14 April 2010:

Paul Levy (Birmingham). Nondeterminism, fixpoints and bisimulation

Yoshiki Kinoshita (AIST). Hoare in Agda

Guy McCusker (Bath). Modelling local variables: possible worlds and

object spaces

Temesghen Kahsai (Swansea). Property preserving development and

testing for Csp-Casl

Makoto Takeyama (AIST). Assurance Cases in Agda

List of talks in Small Research Workshop on Type Theory and Adga in Swansea:

Yoshiki Kinoshita (AIST). Hoare in Agda

Makoto Takeyama (AIST). Assurance Cases in Agda

Karim Kanso. Model Checking from a Type Theory Platform

Fredrik Forsberg. Inductive-Inductive Definitions

Postgraduate seminars are held in Friday afternoon, mostly by postgraduate students of Bath. I attended the following talks.

**23 Apr.**

http://www.bath.ac.uk/comp-sci/research/seminars/view_seminar.php?ID=268

Tom Saunders (Bath). Estimating Egomotion from Dynamic Scenes

Laura Benton (Bath). Participatory Design and Autistic Spec-

trum Disorders

**30 Apr.**

http://www.bath.ac.uk/comp-sci/research/seminars/view_seminar.php?ID=269

Iryna Tsimashenka (Bath). Sliding DFT and Parallel Processing

David Pickup (Bath). Modelling fluids from video

**7 Apr.**

http://www.bath.ac.uk/comp-sci/research/seminars/view_seminar.php?ID=270

Joanna Bryson (Bath). Time for AI

Theory seminar is a series of seminar run by the heory group of the department. It is usually held on Thursday afternoon, often jointly with Swansea via videoconference system. I attended the following talks:

Alan M. Frisch (University of York). The Rules of Modelling Auto-

matic Generation of Constraint Programs

http://www.bath.ac.uk/comp-sci/research/seminars/view_seminar.php?ID=258

Ana (Bath). ....

Agenda:

Yoshiki Kinoshita. Introduction to Dependability Research at AIST

Makoto Takeyama. Assurance Cases in Agda

Lukasz Cyra.

Luke Emmet. Next Version of ASCE system

Luke Emmet. Assurance Cases Standardisation Activity in OMG

Bev Littlewood and Andrey Povyakalo. Confidence models - conser-

vative yet useful?

Lorenzo Stringini. Dealing with adaptation and biases

Martin Churchill showed me his recent work with Dr. Jim Laird about properties of the category of games. Our discussion went on for more than three hours, so it was significant. After obsorbing the idea, I had some comments later during this trip about the difference of study on construction of models and that on structures. I tried to convey it to Martin and I think I succeeded.

I had some discussion with Dr. Anton Setzer about institutional collaboration between Swansea and AIST. We are now even talking about extended collaboration between Bath, Swansea and AIST, as I write in Section 5. One of the themes which Swansea and AIST can collaborate is about research and developement of proof assistants. Both Swansea and AIST has some work using Agda and AIST has participated in development as well. So research and development of Agda could be one of the themes. On the other hand, there are users of other proof assistants in both sites, so we do not have to stick to Agda but themes related to proof assistans in general, for instance, would do as well. During this visit, we had some exchange of ideas concerning plug-in mechanism for putting automatic prover into Agda.

Our presentation (see above) invoked some interest in comparison to GSN. Also, the idea of ¿dealing with unexpected risks¿ attracted much interest of Prof. Lorenzo Stringini. Prof. Robin Bloomfield and I had talked about the next international workshop on assurance cases to be held in Washington; the curren plan is to focus on the problem around the supply chain of software. We will see whether we could offer some talks in the next workshop.

During this trip, I have also visited three other sites in Britain, each in a day trip from Bath. There were seminars in Swansea and CIty University, and those have been described above. We describe here the remaining one, my visit to Queen Mary.

**Swansea (15 Apr).** Small Research Workshop on Type Theory and Adga

**City University, London (21 Apr).**

**Queen Mary College, University of London (4 May).** I met Prof. Edmund Robinson, the head of the department of computer science, after several years of absense, and exchanged recent information on our own work. I talked about our industrial collaboration with more than ten companies accomplished in the past ten years. Prof. Robinson talked about, amongst others, their collaboration with Microsoft about automatic prover for device drivers; control flow was done by Microsoft and data flow was done by Queen Mary, based on separation logic and bunched implication logic. Queen Mary also has works on security and planning based on Baysian network, both of which are quite related to our work. So, it seems worthwhile to have more exchange with Queen Mary, as we (AIST) have now many experiences with industry which could effectively use their results of recent study.

This trip is the end of our two year collaboration project with the support from PMI2. Not only that the both side considers the collaboration as a success, but in fact our collaboration is now being extended to Swansea. Incidentally, we started in this April a ¿collaborative chairnnn¿ in Nara Advanced Institute of Science and Technology, I being the professor of that chair and Hitoshi Ohsaki being the associate professor. Our collaboration may even include Nara, if appropriate.