The first two workshops on the grant were very successful. So when we heard that Yoshiki Kinoshita and Makoto Takeyama would visit Europe for other reasons in February/March 2009, we decided to take the opportunity to run a third workshop on 3rd/4th March. We then took advantage of the concurrent visit to Bath by John Longley from the University of Edinburgh as well as some visitors from the University of Swansea, and, to avoid interruption, we held the second day off-site.
.Prof Guy McCusker
.Dr John Power
.Dr Jim Laird
.Dr Dalia Khader
.Ms Ana Carolina Martins Abbud
.Mr Martin Churchill
.Mr Adam Gundry
.Dr Yoshiki Kinoshita
.Dr Makoto Takeyama
3rd March, Bath:
In Rm 1WN3.12
11:15 Makoto Takeyama: Mini-TT
We present Mini-TT, a small functional language with dependent types. Mini-TT is a step towards a simple and definitive core
language for the proof-assistant Agda based on versions ofMartin-L¿of Type Theory. It is difficult to give a semantics
directly to the full Agda language with advanced features such as synthesis of implicit arguments. Mini-TT will be used as the target
of a translation from the full language, with which the Agda language will be specified and the implementation verified. Mini-TT
contains data types, mutual recursive / inductive definitions and a universe of small types. The syntax, semantics and type system is
specified in such a way that the implementation of a parser, interpreter and type checker is straightforward (around 400 lines in Haskell).
12:00 John Longley: Eriskay: a programming language based on game semantics
2:00 Yoshiki Kinoshita: Overview of DEOS dependability standard project
Our project "User Oriented Dependability" started in October 2008, as one of the project of the programme DEOS (Dependable Embedded
Operating System), which is conducted under CREST scheme of JST (Japan's Agency for Science and Technology). We outline our plan of
the project in four items: (1) clarification of the concept of user oriented dependability, (2) standardisation of the concept clarified
in (1), (3) providing guideline for conformance evaluation and (4) providing guideline for development of dependable system lifecylces.
In Rm 8W2.21
3:15 Anton Setzer: Coalgebras and Codata in Agda
In Rm 8W2.20
4:15 Martin Churchill: A Concrete Representation of Observational Equivalence for PCF
The full abstraction result for PCF using game semantics requires one to identify all innocent strategies that are "innocently indistinguishable". This involves a quantification over all innocent tests, cf. quantification over all innocent contexts. Here we present a concrete representation of innocent strategies (and hence PCF terms) that equates precisely the terms that are observationally equivalent without any need for such quotienting.
4th March, off-site:
12:15 Yoshiki Kinoshita: Introduction to AIST, CVS and CFV
I will overview our affiliation AIST (National Institute of Advanced Industrial Science and Technology) and its research center CVS (Research Center for Verification and Semantics), as well as recently started facility CFV (Collaborative Facilities for Verification). CVS is the research center where we work and it has 39 members in total as of today, including support staffs. CFV are the facilities we are building in AIST. It consists of a cluster computer designed for symbolic computing such as model checking and automatic theorem proving, as well as human resources including supporting body run by 'Kansai Economic Federation,' of which NTT West, Panasonic, Sharp, Kyocera, Omron are active member.
2:00 Makoto Takeyama: Model-based testing of System LSI using Agda
2:45 John Power: Towards a Geometric Foundation for Game Semantics
Geometry has long played a foundational role in the description of categories with variants of monoidal structure. For instance, the free braided monoidal category on 1 is given by the category of braids, i.e., the category of downward-pointing strings in 3-space, and the free tortile category on 1 is given by a category of ribbons. Researchers in game semantics also draw pictures to describe maps in categories of games, but their formalism for categories of games has been combinatorial. So, in the spirit of the development of braided monoidal categories, we refine the combinatorial foundation for game semantics by giving a geometric one that more closely resembles blackboard practice. Specifically, we give a geometric account of the categories of schedules and O-heaps.
4:00 Yoshiki Kinoshita: Applications of Agda
This is a very informal introduction to on-going applications of Agda, done as research projects in CVS. I can show some code if necessary, although I cannot go into detail as I myself is not writing them.