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:&nbs=
p; 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 =
Davenport

Jim Laird

Guy McCusker

John Power

From Oxford:

=20Chris Broadbent

=20From Southampton:

=20Ross Horne

=20From Swansea:

=20Arnold Beckmann

Jin Cao

Karim Kanso

Oliver Kullmann

Ebrahim Larijani

Peter Mosses

Mark New

Monika Seisenb=
erger

Anton 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= ¿-calculus,

=20

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

research. The community is split i= nto those who believe this problem - which is

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

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

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

=20

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

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

proved within a certain fragme= nt of Bounded Arithmetic, necessarily admit a

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

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

the complexity of parity games (and in turn the ¿-calculus model = checking problem):

that they lie in the class of Polynomial Local Sea= rch problems. This result is based

on a new proof of memoryless deter= minacy which can be 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 th= e problem and some other

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

polynomial-time solution unlikely accor= ding to 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 lang= uage usually involves

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

auxiliary entities often need t= o be propagated unchanged between premises and conclusions.

The stand= ard technique is to make such propagation explicit, using variables. Howeve= r,

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

tedious, and it hinders direct reuse of rules in dif= ferent language 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 mentio= ned. The main benefits

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

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

SOS, but avoi= ds the notational overhead of grouping auxiliary entities together in label= s.After motivating and explaining implicit propagation, we consider the fo= undations of

SOS and Modular SOS specifications, and define the meani= ng of SOS specifications

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

implicit propagation can simplify = various 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 informa= l

specification is used to generate items for verification of

l= ower-level detailed designs. Engineers generating those verification<= br /> items often face the problems of informality. Ambiguities, impl= icit

assumptions, inconsistencies, etc. in the specification lead to = wrong

verification items or critical omission. Informality mean= s that the

generation is basically a manual process prone to simple e= rrors.

Besides those reliability issues, the cost of manual generatio= n is a

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

specific= ations. The target specification for this study is that of a

sy= stem LSI under development at Renesas Technology Corp.

Anton Setzer: Proofs by Guarded Recursion

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

=20

and (inductively defined) algebraic types. In order to m= odel concepts like interaction

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

defined) weakly final coa= lgebras to MLTT.

We introduce formation, introduction, elimination, a= nd equality rules for weakly

final coalgebras in MLTT. We will show t= hat guarded induction is nothing but an

informal description of the i= ntroduction rules for weakly final coalgebras.

We investigate the dua= lity between algebraic and coalgebraic types in those rules:

For alge= braic types the introduction rules are simple and predicative,

the el= imination rules involve some degree of impredicativity.

There is a la= rge variety of possible elimination rules, all of which are derived

f= rom the principle of having a least set closed under the introduction rules= .

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

the introduction rules involve some degree of impredica= tivity. There is a large

variety of possible introduction rules, all = of which are derived from the principle

of having the largest set all= owing the elimination principle.We introduce a model of the extension of MLTT by weakly final coalgebras= , and

=20

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

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

coalgebra. We demonstrate that proofs by guarded induction of b= isimulation form

a much more intuitive way of proving bisimulation pr= operties than the usual proofs

based on the introduction of a bisimul= ation 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 softwar= e tools that

can improve the upper development scene of software prod= uct.

This aims to formalize a unified form of specifications of Embed= ded

Software in a proof assistant system Agda, and develop tools whic= h

assist in writing such formalized specifications.