REDO: Redesigning Logical Syntax

Every speaker has a slot of 45 minutes. These 45 minutes ideally should consist of a talk of 30 minutes and a following discussion of 15 minutes.

Time	Tuesday, September 14, 2010
14:00-14:30	Welcome and Coffee (?)
14:30-15:15	Distinguished Invited Guest Speaker: Kai Brünnler
15:15-15:45	Coffee (?) Break
15:45-16:30	Ana C. Calderon
16:30-17:15	Tom Gundersen
17:15-18:30	Open Discussion

Time	Wednesday, September 15, 2010
09:00-09:30	Welcome and Coffee (?)
09:30-10:15	Nicolas Guenot
10:15-10:45	Coffee (?) Break
10:45-11:30	Dale Miller
11:30-12:15	Martin Churchill
12:30-14:30	Lunch
14:30-15:15	Pierre Clairambault
15:15-15:45	Coffee (?) Break
15:45-16:30	Richard McKinley
16:30-17:00	REDO business meeting
17:00-18:30	Open Discussion

Time	Thursday, September 16, 2010
09:00-09:30	Welcome and Coffee (?)
09:30-10:15	Robert Rothenberg
10:15-10:45	Coffee (?) Break
10:45-11:30	Lutz Straßburger

Kai Brünnler (Universität Bern)
Title: The missing structural quantifier Ordinary sequents may have structural conjunction (comma on the left), implication (the entailment sign) and disjunction (comma on the right). They have no structural quantifiers. That's fine for classical predicate logic, of course. Here, fresh free variables and universally quantified variables are essentially the same thing and thus the standard universal-right-rule does the job. However, when we move to non-classical predicate logics (such as free logic or certain modal predicate logics), then the standard universal-right-rule is often too strong or too weak -- and it is not clear how to adapt the rule. It turns out that adding the missing structural quantifier allows us to formulate rules of the desired strength.

Ana C. Calderon (University of Bath)
Title: Understanding Game Semantics through Coherence Spaces Game Semantics is a flexible and accurate way to give semantics to a programming language, however its underlying mathematics is awkward. For example, the proofs that strategies compose associatively and maintain properties imposed on them such as innocence are intricate and require a lot of attention. The work presented at this talk is part of a body of work aimed at understanding Game Semantics at a more abstract level. Our contribution is the existence of a full symmetric monoidal embedding of a category of games into a category whose maps are given by relations. This work is joint with Guy McCusker

Martin Churchill (University of Bath)
Title: A Logic of Sequentiality
Abstract: It is well established through the Curry-Howard isomorphism that functional programs have a correspondence with proofs in intuitionistic logics; we say the corresponding functional program is the computational content of the proof. But what kind of proofs exist whose computational content is an imperative, perhaps object-orientated, program? To answer this question, it is natural to look at denotational models of such languages, of which the primary examples are games models. Here we present a new affine logic WS where proofs represent history-sensitive winning strategies, and hence imperative programs. We can embed (for example) Polarised Linear Logic inside WS, but we also obtain new proofs that correspond to imperative programs. Using categorical properties of the model we obtain a full completeness result: a semantics-guided proof search procedure ensuring each history-sensitive strategy is the semantics of a unique cut-free core proof. We can use this result to derive an explicit cut elimination procedure.

Pierre Clairambault (PPS, Paris and University of Bath)
Title: Strong functors, interleaving ﬁxpoints and game semantics Abstract: In this talk, I will present a sequent calculus \muLJ with induction and co-induction, at the intersection of the \mu-calculus and the intuitionistic sequent calculus LJ and I will show how HO game semantics and parity winning conditions can be combined to give a precise denotational model for it. I will first describe this model for a "weak" fragment of \muLJ, where one can only iterate closed terms. Extending the model to the full rule set of \muLJ requires one to prove that open types are interpreted as strong functors, and to examine how initial algebras and terminal algebras are preserved by functorial liftings. Following these ideas, I will show how to extend the games mentioned above for the full rule set of \muLJ.

Anupam Das (University of Oxford and University of Bath)
Title: Fluid Flows in Dual Tap Systems cancelled

Dale Miller (INRIA Saclay - Île-de-France and LIX, Palaiseau)
Title: Towards a broad spectrum proof certificate Proof assistants and automated theorem provers generally produce evidence of a successful proof in an assortment of (often ad hoc) formats. The extent to which one prover can understand and check such evidence from another prover is the extent to which they can successfully inter-operate. I will outline some recent work on providing a single proof system that can be tuned so that it can host proof systems such as sequent calculus, natural deduction, tableau, and tabled deduction for classical and intuitionistic logics. A proof checker for the hosting proof system can then immediately be a proof checker for all of these other proof systems. The hope is that such a flexible format for proof certificates can be the basis of a lingua franca among proof systems. Central to this work is the use of linear logic and focused proof systems.

Robert Rothenberg (University of St Andrews)
Title: Comparing proof-theoretic formalisms Gentzen-style sequent calculi have been extended in several ways so as to obtain cut-free calculi for various non-classical logics. These extensions are based on changing particular syntactic features of sequent calculi. These extensions may contain structures which do not translate directly into formulae of the logics that these calculi are intended for. This makes translation between formalisms problematic. We discuss these issues, and include results from translating between two kinds of extension, hypersequent and labelled calculi.

François Lamarche (LORIA, Nancy)
Title: Confluence criteria for rewriting on structures with non-trivial automorphisms cancelled

Nicolas Guenot (LIX, Palaiseau)
Title: From lambda-terms to abstract machines via typing The Curry-Howard correspondence is the fundamental basis of functional programming, which allows the introduction of logic, and proof theoretic techniques, in the development of safe programming languages. I will show how this can be pushed forward to the implementation level of abstract machines, where the deep inference methodology allows for a uniform treatment of evaluation orders, and could bring low-level aspects such as program optimisation into the realm of logic.

Tom E. Gundersen (INRIA Saclay - Île-de-France and LIX, Palaiseau)
Title: Counting Pigeons abstract tba

Richard McKinley (Universität Bern)
Title: Path breaking and analyticity in proof nets Atomic flows are a new approach to proof transformation due to Guglielmi and Gundersen; it has been used to define new normal forms for proofs in deep inference formalisms, and guides the design of algorithms yielding those normal forms. The atomic flow of a derivation is a graph indicating the flow of atoms in a derivation, as they are created, destroyed and duplicated. A striking property of the atomic flow approach is its modularity. Atomic flows are not themselves derivations; the operations of normalization are first defined on them, and then shown to be liftable to a genuine deductive system. It would be particularly appealing if the same basic reduction mechanism could be applied to many deductive systems, but so far as I know lifting has only been shown for deep inference systems. In this talk, I will demonstrate how the path-breaker, a particularly simple reduction on atomic flows, can be lifted in a very intuitive way to a class of two-sided proof-nets for classical logic, similar to that studied by Blute et. al for MLL.

Lutz Straßburger (INRIA Saclay - Île-de-France and LIX, Palaiseau)
Title: What is the Problem with Proof Nets for Classical Logic? This talk is supposed to be an informal (and nonexhaustive) overview over some existing notions of proof nets for classical logic, and gives some hints why they might be considered to be unsatisfactory.

REDO: Redesigning Logical Syntax

Meeting from September 14 to September 16, 2010, Bath, UK

Overview

Participants

Programme

Abstracts of Talks

Venue

Organization

Local Organization