Workshop

Royal Society International Exchanges

Bath 13–14 May 2014

9:30–11:30 *Stefano Berardi*

*Recursive Game Theory for Classical Arithmetic*

First part of a graduate-level course on games semantics and the constructive content of classical and intuitionistic logic.

Slides (preliminary draft)

11:30 Coffee

11:45–12:45 *Mauro Piccolo*

*Towards New Foundations for Reversible Programming Languages*We build up from the work by Yokoyama, Axelsen and Gluck "Principles of a reversible programming language" in order to introduce a denotational semantics of a high level imperative reversible language called Janus. We prove that the denotational model is correct with respect to the operational semantics providing an abstract tool to study program equivalence in the Scott-Strachey sense. This could be a point of departure to extend Janus with reversible higher order programming features.

14:15–15:15 *Felice Cardone*

*Executing String Diagrams*

A speculative exploration of the possibility of playing a form of token game over a string diagram, and of the equations that arise from this operational approach. It turns out that the resulting equational theory is compatible with that arising from the geometric approach of Joyal and Street.

15:15 Coffee

15:30–16:30 *Luca Paolini*

*Towards an Algorithmic Characterization of Reversible Computations*

Reversible computing has been characterized by means of non-copositional reversible-automata (reversible TM). We are exploring the possibility of a more abstract approach that would simplify foundational reasoning on invertible recursive functions.

16:30 Coffee

16:45–17:45 *Alessio Guglielmi*

*BV and Cut Elimination in Deep Inference*

First part of a two-hour graduate course. I will introduce the commutative/noncommutative linear logic BV in terms of a naif space-temporal model. BV improves on the ability of linear logic to model spatial structure by satisfactorily capturing temporal structure in programming languages and quantum physics. I will define BV as the most liberal deduction system obtainable from relation webs, which are a generalisation of collapsible orders. This construction naturally leads to the notion of deep inference. This talk might help to understand tomorrow's talk by Bruscoli and Roversi.

Survey

Paper

9:30–11:30 *Stefano Berardi*

*Recursive Game Theory for Classical Arithmetic*

Second part of a graduate-level course on games semantics and the constructive content of classical and intuitionistic logic.

Slides

11:30 Coffee

11:45–12:45 *Paola Bruscoli and Luca Roversi*

*On the Nondeterministic Choice of CCS in Logical Form*We continue to develop a project initiated years ago by establishing the first strict correspondence of a small fragment of CCS with a logical system in deep inference. On this occasion we report on some ideas that would allow to extend that initial fragment in order to handle the choice-operator of CCS.

14:15–15:15 *Alessio Guglielmi*

*BV and Cut Elimination in Deep Inference*

Second part of a two-hour graduate course. I will prove cut elimination in BV by using the 'splitting' technique and I will show that deep inference is the only formalism that can provide an analytic system for a linear logic with a noncommutative self-dual connective, by showing a counterexample due to Alwen Tiu.

Paper 1- Paper 2

15:15 Coffee

15:30–16:15 *Willem Heijltjes*

*The atomic lambda-calculus*

The key to efficient implementation of the lambda-calculus is sharing: using a single stored term to represent many similar ones, and computing with it once, instead of computing on each instance. This is the principle behind explicit substitution calculi, labelled calculi, sharing graphs, and related formalisms.

The atomic lambda-calculus is an implementation of sharing in the lambda-calculus that exhibits a unique combination of features. It is a typed term calculus that implements duplication atomically, one constructor at a time. The calculus achieves fully lazy sharing, and preserves strong normalisation w.r.t. the lambda-calculus.

In this talk I will show how the calculus is obtained as a Curry-Howard interpretation of intuitionistic logic in deep inference. Atomicity is a typical feature in deep-inference formalisms, and derives from the medial inference rule.

This is joint work with Tom Gundersen and Michel Parigot.

Paper 1- Paper 2

16:15 *Coffee and informal discussions*

- Andrea Aler Tubella
- Stefano Berardi
- Paola Bruscoli
- Felice Cardone
- Etienne Duchesne
- Alessio Guglielmi
- Willem Heijltjes
- Jim Laird
- Luca Paolini
- Mauro Piccolo
- John Power
- Luca Roversi
- Daniel Schmitter

You might need a campus map and instructions on how to get to the University of Bath.

Paola Bruscoli and Alessio Guglielmi. The meeting is part of this project.

7.5.2014 Alessio Guglielmi email