Message-ID: <296998153.19967.1561021403729.JavaMail.confluence@wiki1> Subject: Exported From Confluence MIME-Version: 1.0 Content-Type: multipart/related; boundary="----=_Part_19966_1027362485.1561021403729" ------=_Part_19966_1027362485.1561021403729 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Content-Location: file:///C:/exported.html Martin Churchill's second visit to AIST

Martin Churchill's second visit to AIST

In January 2010, Martin Churchill (a PhD student at the Universi= ty of Bath) made a second visit to the CVS site in Osaka. The main purpose = of this trip was to continue working with Makoto Takeyama on formalising so= me of Martin's recent work in the proof assistant (and dependently-typed fu= nctional programming language) Agda.

=20

The recent work in question concerns a Logic of Sequentiality a= nd its related semantics. It is well-known that game semantics is well suit= ed to modelling higher-order imperative programs. Thus, one may give semant= ics of a higher-order imperative program as a strategy on a game. Logic= of Sequentiality attempts to give a logical characterisation of these= strategies. In particular, it provides a proof system WS where formulas re= present (finite) games, and proofs represent (total) strategies on these ga= mes. Further, this system has a set of core rules satisfying the property t= hat proofs of a given formula using only these core rules are in one-to-one= correspondance with total strategies on the denotation of that formula (full completeness).

=20

A general aim of this work is as follows:

=20
=20
• Formalise this proof system
• =20
• Formalise some game semantics, and the semantics of proofs as strategie= s
• =20
• Provide an environment for "running" a given strategy, where the user e= nters the environment-moves and the system responds according to that strat= egy
• =20
=20

In the two-weeks of Martin's visit at AIST, a sucessful start to this ha= s occurred. We have so far:

=20
=20
• Formalised game semantics in Agda (including games, strategies, mediati= ng copycat strategies, composition...)
• =20
• Formalised the system WS from A Logic of Sequentiality
• =20
• Formulated a "semantic function" taking a proof to its corresponding st= rategy for WS
• =20
• Provided a notion of Annotated Game, allowing textual data to be added = to moves for purposes of "running" them
• =20
• Implemented this in the case of the semantics of WS, where a move is an= notated with the formula representing the "rest of the game" to be played=20
• Provided the ability to print out (annotated) games as a tree
• =20
• Provided an environment to "run" strategies on annotated games, as desc= ribed above.
• =20
=20

=20
=20
• Formalising the cut elimination procedure of core-WS (but not completed= its soundness proof)
• =20
• Encoding part of the full completeness theorem (extracting a proof from= a strategy)
• =20
=20

On February 2nd, Martin presented a talk entitled Game Semantics and= Agda at the Osaka Software Engineering Workshop at CVS.

=20

There are some ends that need tying up, and Takeyama-san's visit in Apri= l will be a useful opportunity to do this. Further continuations include fo= rmalising proofs about WS in Agda (such as full completeness and soundness = of cut).

=20

In addition, Martin spoke with other researchers in AIST about their res= earch interests, and this will continue in March/April as a number of these= researchers visit Bath.

=20

A snapshot of this work can be found at http://people.b= ath.ac.uk/mdc25/AgdaWS

=20

Postscript (16.09.10)

=20

In further collaborations between Martin, Makoto and others, we have now= also done the following:

=20
=20
• Formalised a finitary imperative language and its embedding into WS (he= nce this gives a way to calculate the concrete strategy, and core proof, as= sociated by a program)
• =20
• Restructured the full completeness procedure to also contain its termin= ation proof, and hence pass Agda's termination checker.
• =20
• Explored the feasibility of formalising infinite games and partial stra= tegies in Agda, and completed this to the extent to this is practical in th= e current version of Agda. This was done at the twelfth Agda Implementors Meeting
• =20
------=_Part_19966_1027362485.1561021403729--