...

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

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

...

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

Here, we first introduce a notion of bisimulation based on the distinction between computations and values, with a corresponding liberal congruence format. We then provide metatheory for a modular variant of SOS (MSOS) which provides a systematic treatment of auxiliary entities. This is based on a higher order form of bisimulation, and we formulate an appropriate congruence format. Finally, we show how algebraic laws can be proved sound for bisimulation with reference only to the (M)SOS rules defining the programming constructs involved in them. Such laws remain sound for languages that involve further constructs.

** Anupam Das: A new proof of the propositional pigeonhole principle, for weak monotone systems:** The pigeonhole principle 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 propositional tautologies, PHP, that has become a benchmark in proof complexity in the last few decades.

Atserias, Galesi and Gavalda have constructed quasipolynomial-size proofs of PHP in the monotone (i.e. negation-free) sequent calculus, based on propositional encodings of certain counting functions. We use a similar approach here to obtain quasipolynomial-size proofs in the fragment free of cuts between ancestors of contraction and weakening steps.

Our argument operates in an equivalent system of the deep inference proof methodology, known to be equivalent to the aforementioned fragment of sequent calculi, where normalisation procedures are more suitable for the task at hand, due primarily to the locality of the inference rules. Our main construction is a formalisation of merge sort in deep inference in order to achieve appropriate permutations of the inputs for the required counting functions.

** Takako Nemoto (JAIST): The proof theoretic strength of determinacy between \Sigma^0_1 and \Delta^0_2:** It is known that determinacy of infinite games in very low level of the Borel hierarchy can be characterized by set comprehensions in second order arithmetic (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 subsystems of second order arithmetic, T. Nemoto, M. O. Medsalem and K. Tanaka, Mathematical Logic Quarterly, Volume 53, Issue 3 (2007), pp. 226 - 236.

...