# Collegium Logicum 2012: Structural Proof Theory

Dates: 15–16 November 2012
Venue: Gilles Kahn room, Alan Turing Building, LIX, Ecole Polytechnique (Directions)

### 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

### 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.