Robert Recorde Room (Far-205), Faraday Building (=3D large blue building= to the right on the campus), at Swansea University.

Lunch at 1pm in Cafe Fusion in Fulton house. Coffee at 1:45 in the Rober= t Recorde Room.

**1:00-2:00: Lunch **

**2:00--2:40: Olle Fredriksson (Birmingham): Abstract machines for=
game semantics, revisited**

**2:40=E2=80=933:20: Martin Churchill (Swansea): Modular B=
isimulation Theory for Computations and Values**

**3:20--3:50: Coffee**

**3:50--4:30: Anupam Das (Bath): A new proof of the propos=
itional pigeonhole principle, for weak monotone systems.**

**4:30--5:10: Takako Nemoto (JAIST): The proof theoretic str=
ength of determinacy between \Sigma^0_1 and \Delta^0_2**

**5:10--5:20: Break**

**5:20--6:00: Peter Schuster (Leeds): Ideal Objects for Finite Met=
hods**

** Olle Fredriksson and Dan Ghica: Abstract machines for ga=
me semantics, revisited: **We define new abstract machines =
for game semantics which correspond to networks of conventional computers, =
and can be used as an intermediate representation for compilation targeting=
distributed systems. This is achieved in two steps. First we introduce the=
HRAM, a Heap and Register Abstract Machine, an abstraction of a convention=
al computer, which can be structured into HRAM nets, an abstract point-to-p=
oint network model. HRAMs are multi-threaded and subsume communication by t=
okens (cf. IAM) or jumps (cf. JAM). Game Abstract Machines (GAM), are HRAMs=
with additional structure at the interface level, but no special operation=
al capabilities. We show that GAMs cannot be naively composed, but composit=
ion must be mediated using appropriate HRAM combinators. HRAMs are flexible=
enough to allow the representation of game models for languages with state=
(non-innocent games) or concurrency (non-alternating games). We illustrate=
the potential of this technique by implementing a toy distributed compiler=
for ICA, a higher-order programming language with shared state concurrency=
, thus significantly extending our previous distributed PCF compiler. We sh=
ow that compilation is sound and memory-safe, i.e. no (distributed or local=
) garbage collection is necessary.

**Martin Churchill: Modular Bisimulation Theory for Computations a=
nd Values**: For structural operational semantics (SOS) of process a=
lgebras, various notions of bisimulation have been studied, together with r=
ule formats ensuring that bisimilarity is a congruence. For programmi=
ng languages, however, SOS generally involves auxiliary entities (e.g. stor=
es) and computed values, and the standard bisimulation and rule formats are=
not directly applicable.

Here, we first introduce a notion of bisimula=
tion based on the distinction between computations and values, with a corre=
sponding liberal congruence format. We then provide metatheory for a =
modular variant of SOS (MSOS) which provides a systematic treatment of auxi=
liary entities. This is based on a higher order form of bisimulation, and w=
e formulate an appropriate congruence format. Finally, we show how algebrai=
c laws can be proved sound for bisimulation with reference only to the (M)S=
OS rules defining the programming constructs involved in them. Such laws re=
main sound for languages that involve further constructs.

=

** Anupam Das: A new proof of the propositional pigeonhole=
principle, for weak monotone systems:** The pigeonhole pri=
nciple states that, if there are n+1 pigeons in n holes, there must be two =
pigeons in the same hole. This can be expressed as a sequence of propositio=
nal tautologies, PHP, that has become a benchmark in proof complexity in th=
e last few decades.

Atserias, Galesi and Gavalda have constructed quasip= olynomial-size proofs of PHP in the monotone (i.e. negation-free) sequent c= alculus, based on propositional encodings of certain counting functions. We= use a similar approach here to obtain quasipolynomial-size proofs in the f= ragment free of cuts between ancestors of contraction and weakening steps.<= br>Our argument operates in an equivalent system of the deep inference proo= f methodology, known to be equivalent to the aforementioned fragment of seq= uent calculi, where normalisation procedures are more suitable for the task= at hand, due primarily to the locality of the inference rules. Our main co= nstruction is a formalisation of merge sort in deep inference in order to a= chieve appropriate permutations of the inputs for the required counting fun= ctions.

**Takako Nemoto (JAIST): The proof theoretic strengt=
h of determinacy between \Sigma^0_1 and \Delta^0_2**: It is known that determinacy of infinite games in very low level of the B=
orel hierarchy can be characterized by set comprehensions in second order a=
rithmetic (cf: [1] and [2]). In this talk, we consider the proof theoretic =
strength of determinacyschemata between \Sigma^0_1 and \Delta^0_2.

[1] =
Subsystems of Second order arithmetic 2nd edition, S. G. Simpson, Cambridge=
University Press

[2] Infinite games in the Cantor space and subs=
ystems of second order arithmetic, T. Nemoto, M. O. Medsalem and K. Tanaka,=
Mathematical Logic Quarterly, Volume 53, Issue 3 (2007), pp. 226 - 236.

**Peter Schuster: Ideal Objects for Finite Methods:** Somew=
hat miraculously, transfinite methods do work for proving quite a few theor=
ems of a fairly finite nature. The corresponding ideal objects are typicall=
y invoked towards a contradiction, and therefore do not really exist (Hendt=
lass).We aim at exploring and exploiting this phenomenon: by reducing trans=
finite proof methods to finite ones, and thus exhibiting the computational =
content of the virtually inexistent ideal objects. This is work in progress=
and follows a bottom-up strategy, i.e. from concrete examples within mathe=
matics to possible metamathematical observations. First case studies have p=
roved sucessful [12, 5]: several theorems that admit short and elegant proo=
fs by contradiction but with Zorn's Lemma have turned out to follow in a di=
rect and elementary way from Raoult's Open Induction [8]. The maximal or mi=
nimal elements characteristic of any invocation of Zorn's Lemma are elimina=
ted, and it is made possible to pass from classical to intuitionistic logic=
. If the theorem has finite input data, then a finite partial order carries=
the required instance of induction, which thus only needs mathematical ind=
uction. Besides the revised Hilbert Programme a la Kreisel and Feferman, in=
spirations come from the work on combinatorics by U. Berger and Coquand [1,=
3]; from Coste, Lombardi, and Roy's dynamical algebra [4]; and from the in=
terplay between pointwise and point-free topology in Sambin's basic picture=
[10]. In particular there are striking parallels to Maietti and Sambin's t=
wo-level foundations with a forget-restore option [2, 7, 6], and to Sambin'=
s appeal for allowing the use of ideal objects in real mathematics once thi=
s is approved by, say, appropriate conservativity [9, 11]. This partially i=
s joint work with F. Ciraulo, N. Gambino, M. Hendtlass, and D. Rinaldi.

1. Ulrich Berger. A computational interpretation of open induction.= In F. Titsworth, editor, Proceedings of the Ninetenth Annual IEEE Symposiu= m on Logic in Computer Science, pages 326-334. IEEE Computer Society, 2004.=

2. Francesco Ciraulo and Giovanni Sambin. Finiteness in a minimalist fou= ndation. In Types for proofs and programs, volume 4941 of Lecture Notes in = Comput. Sci., pages 51-68. Springer, Berlin, 2008.

3. Thierry Coquand. Constructive topology and combinatorics. In Construc= tivity in computer science (San Antonio, TX, 1991), volume 613 of Lecture N= otes in Comput. Sci., pages 159-164. Springer, Berlin, 1992.

4. Michel Coste, Henri Lombardi, and Marie-Francoise Roy. Dynamical meth= od in algebra: Effective Nullstellensaetze. Ann. Pure Appl. Logic, 111(3):2= 03{256, 2001.

5. Matthew Hendtlass and Peter Schuster. A direct proof of Wiener's theo= rem. In S. B. Cooper, A. Dawar, and B. Loewe, editors, How the World Comput= es. Turing Centenary Conference and Eighth Conference on Computability in E= urope, volume 7318 of Lect. Notes Comput. Sci., pages 294-303, Berlin and H= eidelberg, 2012. Springer. Proceedings, CiE 2012, Cambridge, UK, June 2012.=

6. Maria Emilia Maietti. A minimalist two-level foundation for construct= ive mathematics. Ann. Pure Appl. Logic, 160(3):319{354, 2009.

7. Maria Emilia Maietti and Giovanni Sambin. Toward a minimalist foundat= ion for constructive mathematics. In L. Crosilla and P. Schuster, editors, = From Sets and Types to Topology and Analysis, volume 48 of Oxford Logic Gui= des, pages 91{114. Oxford: Oxford University Press, 2005.

8. Jean-Claude Raoult. Proving open properties by induction. Inform. Pro= cess. Lett., 29(1):19-23, 1988.

9. Giovanni Sambin. Steps towards a dynamic constructivism. In P. Gaerde= nfors et al., editor, In the Scope of Logic, Methodology and Philosophy of = Science, volume 315 of Synthese Library, pages 263-286, Dordrecht, 2002. Kl= uwer. 11th International Congress of Logic, Methodology and Philosophy of S= cience. Krakow, Poland, August 1999.

10. Giovanni Sambin. Some points in formal topology. Theoret. Comput. Sc= i., 305(1-3):347-408, 2003.

11. Giovanni Sambin. Real and ideal in constructive mathematics. In Epis= temology versus ontology, volume 27 of Log. Epistemol. Unity Sci., pages 69= {85. Springer, Dordrecht, 2012.

**From Bath: **

Anupam Das

Cai Wingfield

Alessio Guglielmi

Willem Heijltjes

Jim Laird

**From Birmingham:**

Liang-Ting Chen

Olle Fredriksson** **

**From Jaist: **

Takako Nemoto

**From Leeds: **

Peter Schuster

**From Swansea: **

Arnold Beckmann

Ulrich Berger

Jens Blanck

Martin Churchill

Fredrik Nordvall Forsberg

Roger Hindley

Phillip James

Andrew Lawrence

Peter Mosses

Caspar Poulson

Monika Seisenberger

Paolo Torrini

Ferdinand Vesley

**See all Wessex sites involved and meetings so=
far.**