Venue: Gilles Kahn room, Alan Turing Building, LIX, Ecole Polytechnique (Directions)

[Jump to Program]

### Theme

The topic of the workshop is structural proof theory and it is open to anyone interested. Proposals for contributed talks, including talks on work in progress and discussions of open problems, are welcome.

### Invited Talks

**Alex Simpson**:*Cyclic Arithmetic (in context)*In this talk, I shall extend Peano Arithmetic by admitting a class of finitely presented infinite proofs, formalizing a notion of proof by infinite descent (Fermat’s “descente infinie”). The main result is that, in doing so, we get Peano Arithmetic back again.The point of this somewhat circular exercise is to shed light on a more general problem: that of relating “cyclic proofs” to proofs with explicit (co)induction. Insofar as time permits, I shall discuss some instances of this broader problem, by considering various contexts in which notions of “cyclic proof” arise.

**Paulo Oliva**:*Algorithms from proofs in classical arithmetic and analysis*In this talk we will see how one can use Gödel’s functional interpretation combined with the negative translation in order to obtain effective algorithms from non-constructive proofs in arithmetic and analysis. We will start by looking at the interpretation of classical principle such as excluded middle and the drinker’s paradox. Then, the technique will be further explained through the analysis of concrete proofs of the following theorems

- infinite pigeon-hole principle
- bounded collection
- no injection from Baire space to natural numbers

Most of the analysis will make use of the so-called selection functions and their corresponding product [1,2], which are also going to be explained in the talk.

[1] M. Escardó and P. Oliva. Sequential games and optimal strategies

Proceedings of the Royal Society A, 467:1519-1545, 2011[2] M. Escardó and P. Oliva. Selection functions, bar recursion and backward induction

Mathematical Structures in Computer Science, 20(2):127-168, 2010

### Contributed Talks

- Federico Aschieri:
*Interactive realizability for Peano Arithmetic with Skolem Axioms* - Matthias Baaz:
*On the limits of analyticity* - Jaime Gaspar:
*Completeness of Heyting/Peano arithmetic with the ω-rule* - Stéphane Gimenez:
*The reducibility method in Calculus of Structures* - Stéphane Graham-Lengrand:
*Psyche, an implementation of focused sequent calculus used as a generic proof-search platform* - Nicolas Guenot:
*On the computational contents of proofs in deep inference* - Willem Heijltjes:
*An Atomic Lambda Calculus* - Alexander Leitsch:
*CERES for First-Order Schemata* - Tomer Libal:
*Choosing Most General Unifiers in Higher-order Resolution* - Revantha Ramanayake:
*Labelled tree sequents, Tree hypersequents and Nested (Deep) Sequents* - Fabien Renaud:
*News from ProofCert* - Giselle Reis:
*CERES in Intuitionistic Logic* - Lara Spendier:
*Automated Support for the Investigation of Paraconsistent and Other Logics* - Lutz Straßburger:
*From Proof Nets to Virtual Tensors — Making Semi-star-autonomous Categories Free* - Daniel Weller:
*Deskolemization, Equality and Logical Complexity*

### Participants

### Schedule

**Thursday, November 15**

(Gilles Kahn room, Alan Turing Building) | |

09:30-10:00 | Coffee |

10:00-11:00 | Alex Simpson: Cyclic Arithmetic (in context) |

11:00-11:30 | Matthias Baaz: On the limits of analyticity |

11:30-12:00 | Willem Heijltjes: An Atomic Lambda Calculus |

12:00-13:30 | Lunch in the Ecole Polytechnique cafeteria |

(Gilles Kahn room, Alan Turing Building) | |

13:30-14:00 | Alexander Leitsch: CERES for First-Order Schemata |

14:00-14:30 | Giselle Reis: CERES in Intuitionistic Logic |

14:30-15:00 | Jaime Gaspar: Completeness of Peano arithmetic with the ω-rule |

15:00-15:30 | Coffee |

15:30-16:00 | Stéphane Graham-Lengrand: Psyche, an implementation of focused sequent calculus used as a generic proof-search platform |

16:00-16:30 | Fabien Renaud: News from ProofCert |

16:30-17:00 | Lara Spendier: Automated Support for the Investigation of Paraconsistent and Other Logics |

20:00- | Workshop dinner Bistrot Victoires 6 Rue la Vrillière, 75001 Paris [ location in google maps ] |

**Friday, November 16**

(Gilles Kahn room, Alan Turing Building) | |

09:30-10:00 | Coffee |

10:00-11:00 | Paulo Oliva: Algorithms from proofs in classical arithmetic and analysis |

11:00-11:30 | Federico Aschieri: Interactive realizability for Peano Arithmetic with Skolem Axioms |

11:30-12:00 | Tomer Libal: Choosing Most General Unifiers in Higher-order Resolution |

12:00-13:30 | Lunch in the Ecole Polytechnique cafeteria |

(CMAP conference room, 2nd Floor, Aisle 0 — map and directions will be provided in the morning session) | |

13:30-14:00 | Lutz Straßburger: From Proof Nets to Virtual Tensors — Making Semi-star-autonomous Categories Free |

14:00-14:30 | Stéphane Gimenez: The reducibility method in Calculus of Structures |

14:30-15:00 | Nicolas Guenot: On the computational contents of proofs in deep inference |

15:00-15:30 | Coffee |

15:30-16:00 | Daniel Weller: Deskolemization, Equality and Logical Complexity |

16:00-16:30 | Revantha Ramanayake: Labelled tree sequents, Tree hypersequents and Nested (Deep) Sequents |

### Support and Organization

This workshop will be hosted by the Laboratoire d’Informatique (LIX) and by INRIA Saclay. Funding is provided by the ANR-FWF project STRUCTURAL and by the Kurt Gödel Society.

The workshop is being organized by Stefan Hetzl and Kaustuv Chaudhuri.