Pisa Summer Workshop on Proof Theory

Pisa, Italy, 12-15 June 2012

Organizers: Department of Philosophy, University of Pisa;
Department of Philosophy, University of Helsinki

Call for papers

Aimed at understanding the structure of mathematical proofs, proof theory has undergone different phases: it has been reductive, general, structural. Especially thanks to sequent calculus formalizations, deep results were attained as far as proofs in pure logic and arithmetic are concerned. Through significant connections with computer science, proof theory contributed to the birth of new areas of research outside traditional mathematics, such as the verification of correctness of computer programs. Natural deduction has led to the Curry-Howard correspondence and to connections with functional programming, and sequent calculus is often used in systems of automatic proof search, as in logic programming. Rooted in general proof theory, a proof-theoretic semantics has been recently developed as an alternative to standard denotational truth-condition semantics. The workshop will focus mainly on proof systems, but we aim at touching several areas of proof-theoretical research.
The workshop will be framed in two six-hour tutorials, six one-hour lectures, and is open to half-hour contributed talks. People interested to present a paper in the workshop may send a title with a short abstract to one of the following e-mail addresses:


New: List of contributed talks

Tutorial speakers: :

Invited speakers :

Participants: To be announced



Dipartimento di Filosofia, via Paoli 15, Pisa

Social programme and practical information (accommodation, transport, etc.):

Social dinner on Thursday 14 at 20.00: Ristorante la Clessidra, via del Castelletto 26/30, directions
Official Tourism Website for Pisa Province
Civic Network Pisa
Visit Pisa
Please notice that the Workshop takes place in a very special time of the year for the town of Pisa, being so close to the celebration of the patron saint's feast day:
La luminara
The magic of the luminara
Therefore, we warmly recommend you to reserve your accommodation as soon as possible.
Though there is no formal agreement or committment, the following hotels have been informed and will be glad to accommodate partecipants of Pisa Summer Workshop:
Hotel Leonardo Pisa
Hotel Royal Victoria
Hotel Verdi
Gand Hotel Bonanno

Registration (early registration deadline May 30)



  • George Metcalfe (University of Bern): Admissible Rules in Logic and Algebra

  • Sara Negri (University of Helsinki): Proof Systems for Modal and Epistemic Logics

  • Invited talks:

  • Arnon Avron (University of Tel Aviv): Construction of Cut-free Sequent Calculi for Paraconsistent Logics
    • Abstract: We describe a general method for a systematic and modular generation of cut-free calculi for thousands of paraconsistent logics. The method relies on the use of non-deterministic semantics for these logics.

  • Kosta Dosen (University of Belgrade): The Main Question of General Proof Theory
    • Abstract: General proof theory deals with the structure of proofs, as exhibited, for example, in the Curry-Howard correspondence, and not with the strength of proofs measured by ordinals, which is what one finds in proof theory that arose out of Hilbert's programme. This theory addresses the question "What is a proof" by dealing with questions related to normal forms of proofs, and in particular with the question of identity criteria for proofs, which may be found, at least implicitly, in Hilbert's 24th problem. In general proof theory one looks for an algebra of proofs, and for that one concentrates on the operations of this algebra, which come with the inference rules. As an equational theory, the algebra of proofs involves the question of identity criteria for proofs, the main question of general proof theory. Much of general proof theory is the field of categorial proof theory, where through results called coherence results, which provide a model theory for equality of proofs, logic finds new ties with geometry, topology and algebra.

  • Hermann Ruge Jervell (University of Oslo): Cut elimination
    • Abstract: We investigate the combinatorics involved in cut elimination. As a tool we use Gentzen games which is helpful to see why the cut elimination terminate and how we get the estimates of the complexity of cut elimination for various systems.
  • Simone Martini (University of Bologna): Implicit Computational Complexity and the quest for intensional completeness
      Abstract: ICC aims to the description of complexity phenomena based on language restrictions, and not on external measure conditions or on explicit machine models. Proof-theory has given several ICC characterizations of complexity classes, in which any function computed in a certain bound is represented by a proof in the calculus. A system is intensionally complete for a complexity class C if any algorithm computing a function in C is represented by a proof in the calculus.
  • Jan von Plato (University of Helsinki): The interpretation of cuts in natural deduction
    • Abstract: Arbitrary derivations in sequent calculus with cuts are interpreted in terms of natural deduction. The interpretation consists of a translation from sequent derivations to natural derivations.
  • Alex Simpson (University of Edinburgh): Proof systems for intuitionistic modal logics revisited
    • Abstract: For classical modal logic, there is general agreement on the main calculi of interest. Moreover, for most such calculi, well-behaved structural proof systems (e.g., sequent calculi) are available in many styles (e.g., ordinary sequents, hypersequents, labelled sequents, etc.). In contrast, for intuitionistic modal logic, there is no consensus on the main calculi, and, for each choice of calculus, the range of applicable proof styles seems much more constrained. In this talk, I shall present a personal perspective on the state of affairs. One topic I intend to focus on, in particular, is the tension between labelled and unlabelled approaches to modal proof systems.

      Contributed talks

      1. Jesse Alama: Experiments with obvious inferences in formal proofs
      2. Michael Arndt, Laura Tesconi: A Framework of Explicit Composition
      3. Luca Bellotti (joint work with Lorenzo Carlucci): Von Neumann's consistency proof
      4. Agata Ciabattoni (joint work with Matthias Baaz): Proof theory for non-classical logics: a negative result
      5. Vincent Degauquier: Cut-elimination, Excluded Middle and Non-contradiction
      6. José Espírito Santo: Intuitionistic asymmetry: how the classical CBN/CBV duality breaks
      7. Jeroen Goudsmit: Admissible Rules of Gabbay-de Jongh Logics
      8. Bogdan Dicher: Sequent calculus, bilateralism and logical consequence
      9. Antonino Drago: Proof theory in the case of a change in the kind of logic. The crucial role played by Leibniz' principle of sufficient reason
      10. Nissim Francez: Relevant Harmony
      11. Jens Ulrik Hansen: Tableau systems for Hybrid public announcement logic with distributed knowledge
      12. Yoichi Hirai: A Lambda Calculus for Goedel-Dummett Logic Capturing Waitfreedom
      13. Rosalie Iemhoff: Unification in modal and intermediate logics
      14. Roman Krenicky: A 2-Categorical Notion of Proof Equality
      15. Björn Lellmann: Constructing Cut-free Sequent Systems with Context Restrictions
      16. Tadeusz Litak: Extended Curry-Howard correspondence for constructive Loeb logics
      17. Dale Miller: Describing canonical proof structures by abstracting sequent calculus proofs
      18. Pierluigi Minari: Variations on G3K
      19. Alberto Momigliano (joint work with Alessandro Avellone and Camillo Fiorentini): Focusing, Termination and the Gödel-Dummett Logic
      20. Franco Parlamento (joint work with Flavio Previale): The subterm property for the sequent calculus with equality
      21. Dirk Pattinson: Labelled Sequent Calculi for Many-Valued Modal Logics
      22. Luis Pinto (joint work with José Espírito Santo, Ralph Matthes, and Koji Nakazawa): Monadic translation of classical and intuitionistic sequent calculus
      23. Carlo Proietti: Non-classical Modal Logics and tableau testing
      24. Giselle Reis (joint work with Vivek Nigam and Elaine Pimentel): An Extended Framework for Specifying and Reasoning about Proof Systems
      25. Allard Tamminga (joint work with Barteld Kooi): Correspondence Theory for the Logic of Paradox
      26. Luca Tranchini: Proof-theoretic semantics, paradoxes and the distinction between sense and denotation
      27. Diego Valota: Building Strongest Deductive Interpolants in Nilpotent Minimum Logic
      28. Anna Zamansky (joint work with Matthias Baaz and Ori Lahav): Effective Finite-valued Semantics for Labelled Calculi

      Last updated on 24.4.2012 by Sara Negri