↑ Return to Meetings

Collegium Logicum 2012: Structural Proof Theory

Dates: 15–16 November 2012
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

Federico Aschieri
Matthias Baaz
David Baelde
Kaustuv Chaudhuri
Jaime Gaspar
Stéphane Gimenez
Stéphane Graham-Lengrand
Nicolas Guenot
Tom Gundersen
Willem Heijltjes
Stefan Hetzl
Alexander Leitsch
Tomer Libal
Dale Miller
Novak Novakovic
Paulo Oliva
Michel Parigot
Francesca Poggiolesi
Revantha Ramanayake
Giselle Reis
Fabien Renaud
Alex Simpson
Lara Spendier
Arnaud Spiwack
Lutz Straßburger
Daniel Weller

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.