The second meeting of the Wessex Theory Seminar was held on Wedn= esday 17 September 2008, hosted by the University of Bath. Lectures w= ere held in Room 6E 2.2 of the University of Bath's Claverton (Bath) campus= .

=20Lunch and coffee were provided.

=20Talks were expected to last 35-40 minutes, giving time for questions and= change-over. The schedule for the day was as follows, with abstracts below= :

=2011:00 Coffee

=2011:15 Peter Mosses: Implicit Propagation in SOS

=2012:00 Lunch

=201:30 Keishi Okamoto: Formalization of System LSI Specification and=
Automatic Generation of Verification Items

2:15 Arnold Beckmann: =
On the Complexity of Parity Games

3:00 Coffee

=203:30 Shunsuke Yatabe: A new project on formalizing specifications<= br> 4:15 Anton Setzer: Proofs by Guarded Recursion

=205:00 Close

=20From AIST (Japan):

=20Keishi Okamoto

Shunsuke Yatabe

From Bath:

=20Ana C. M. Abbud

Paola Bruscoli

Martin Churchill

James Davenp=
ort

Jim Laird

Guy McCusker

John Power

From Oxford:

=20Chris Broadbent

=20From Southampton:

=20Ross Horne

=20From Swansea:

=20Arnold Beckmann

Jin Cao

Karim Kanso

Oliver Kullmann

Ebra=
him Larijani

Peter Mosses

Mark New

Monika Seisenberger

Anto=
n Setzer

Arnold Beckmann (joint work with Faron Moller): On the complexity = of parity games (BM08)

=20=20=20Abstract: Parity games underlie the model checking problem for the modal= =C2=BF-calculus,

=20

the complexity of which remains unresolved after more= than two decades of intensive

research. The community is split into th= ose who believe this problem - which is

known to be both in NP and coNP= - has a polynomial-time solution (without the

assumption that P=3DNP) = and those who believe that it does not. (A third, pessimistic,

faction = believes that the answer to this question will remain unknown in their life= time.)In this paper we explore the possibility of employing Bounded Arithmetic= to resolve

=20

this question, motivated by the fact that problems which ar= e both NP and coNP, and

where the equivalence between their NP and coNP= description can be formulated and

proved within a certain fragment of = Bounded Arithmetic, necessarily admit a

polynomial-time solution. While= the problem remains unresolved by this paper, we

do proposed another a= pproach, and at the very least provide a modest refinement to

the compl= exity of parity games (and in turn the =C2=BF-calculus model checking probl= em):

that they lie in the class of Polynomial Local Search problems. Th= is result is based

on a new proof of memoryless determinacy which can b= e formalised in Bounded Arithmetic.The approach we propose may offer a route to a polynomial-time solution.= Alternatively,

there may be scope in devising a reduction between the = problem and some other

problem which is hard with respect to PLS, thus = making the discovery of a

polynomial-time solution unlikely according t= o current wisdom.

Peter Mosses (joint work with Mark New): Implicit Propagation in S= OS (MN08)

=20=20=20Abstract: In contrast to a transition system specification in process al= gebra,

=20

a structural operational semantics (SOS) of a programming langua= ge usually involves

auxiliary entities: stores, environments, etc. When= specifying SOS rules, particular

auxiliary entities often need to be p= ropagated unchanged between premises and conclusions.

The standard tech= nique is to make such propagation explicit, using variables. However,

r= eferring to all entities that need to be propagated unchanged in each rule = can be

tedious, and it hinders direct reuse of rules in different langu= age descriptions.We propose a new interpretation of SOS rules, such that each auxiliary e= ntity is

= =20

implicitly propagated in all rules in which it is not mentione= d. The main benefits

include significant notational simplification of S= OS rules and much-improved reusability.

This new interpretation of SOS = rules is based on the same foundations as Modular

SOS, but avoids the n= otational overhead of grouping auxiliary entities together in labels.After motivating and explaining implicit propagation, we consider the fo= undations of

SOS and Modular SOS specifications, and define the meaning= of SOS specifications

with implicit propagation by translating them to= Modular SOS. We then show how

implicit propagation can simplify variou= s rules found in the SOS literature.

Keishi Okamoto: Formalization of System LSI Specification and Auto= matic Generation of Verification Items

=20=20=20Abstract:The design process of a system LSI traditionally starts with

=20

an informal specification in a combination of a natural language and

= some pseudo programming language such as a pseudo C. This informal

specification is used to generate items for verification of

lower-lev= el detailed designs. Engineers generating those verification

item= s often face the problems of informality. Ambiguities, implicit

a= ssumptions, inconsistencies, etc. in the specification lead to wrong

ve= rification items or critical omission. Informality means that the

= generation is basically a manual process prone to simple errors.

Besid= es those reliability issues, the cost of manual generation is a

big iss= ue in the productivity of design processes.We aim at automatic generation of verification items from

specificat= ions. The target specification for this study is that of a

system= LSI under development at Renesas Technology Corp.

Anton Setzer: Proofs by Guarded Recursion

=20=20=20Abstract: Martin-L=C3=B6f type theory (MLTT) is based on the dependent f= unction type

=20

and (inductively defined) algebraic types. In order to mod= el concepts like interaction

or object-orientation in MLTT in a direct = way, it is useful to add (coinductively

defined) weakly final coalgebra= s to MLTT.

We introduce formation, introduction, elimination, and equal= ity rules for weakly

final coalgebras in MLTT. We will show that guarde= d induction is nothing but an

informal description of the introduction = rules for weakly final coalgebras.

We investigate the duality between a= lgebraic and coalgebraic types in those rules:

For algebraic types the = introduction rules are simple and predicative,

the elimination rules in= volve some degree of impredicativity.

There is a large variety of possi= ble elimination rules, all of which are derived

from the principle of h= aving a least set closed under the introduction rules.

For coalgebraic = types, the elimination rules are simple and predicative, whereas

the in= troduction rules involve some degree of impredicativity. There is a largevariety of possible introduction rules, all of which are derived from th= e principle

of having the largest set allowing the elimination principl= e.We introduce a model of the extension of MLTT by weakly final coalgebras= , and

=20

investigate the implications for meaning explanations, namely the= need for types,

the meaning of which is given by an elimination princi= ple.We will then show that bisimulation is an example of a dependent weakly = final

coalgebra. We demonstrate that proofs by guarded induction of bis= imulation form

a much more intuitive way of proving bisimulation proper= ties than the usual proofs

based on the introduction of a bisimulation = relation.

Shunsuke Yatabe: A new project on formalizing specifications

=20=20Abstract: In this talk we introduce a new on-going research project (joi= ntly with

several companies) for developing a methodology and software = tools that

can improve the upper development scene of software product.=

This aims to formalize a unified form of specifications of Embedded

Software in a proof assistant system Agda, and develop tools which

as= sist in writing such formalized specifications.