Sharing and Sequentiality in Proof Systems with Locality
Workshop
Royal Society International Exchanges
Bath 13–14 May 2014
Talks
13 May 2014 morning – Room EB 0.12
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.
13 May 2014 afternoon – Room 1W 3.7
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
14 May 2014 morning – Room EB 0.15
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 May 2014 afternoon – Room EB 0.15
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
People
Location
You might need a campus map and instructions on how to get to the University of Bath.
Organisers
Paola Bruscoli and Alessio Guglielmi. The meeting is part of this project.
7.5.2014 Alessio Guglielmi email