28 January 2016
09:45-10:00 Welcome
10:00-11:00 Ugo Dal Lago - Implicit complexity and the Curry-Howard correspondence (course, part 1)
11:00-11:30 Coffee break
11:30-12:30 Hugo Herbelin - A proof with side effects of Gödel's completeness theorem (course, part 1)
12:30-14:00 Lunch
14:00-14:30 Daniel Graça - A brief introduction to Computable Analysis
14:30-15:00 Andreia Mordido - Probabilistic Logic over Equations and Domain Restrictions
15:00-16:00 João Araújo - The logic of using automated reasoning (course, part 1)
16:00-16:30 Coffee break
16:30-17:00 Filipe Casal - A Nelson-Oppen combination theorem for many-sorted shiny theories
17:00-17:30 Andreia Teixeira - Definitions of Conditional Rényi entropies: a review
17:30-18:00 Bruno Loff - Proofs of space: simplified and optimized

29 January 2016
09:00-10:00 João Araújo - The logic of using automated reasoning (course, part 2)
10:00-10:30 Coffee break
10:30-11:30 Ugo Dal Lago - Implicit complexity and the Curry-Howard correspondence (course, part 2)
11:30-12:30 Hugo Herbelin - A proof with side effects of Gödel's completeness theorem (course, part 2)
12:30-14:00 Lunch
14:00-14:30 Pierluigi Graziani - On the Use and Abuse of Formal Logic in the Study of Euclid's Elements
14:30-15:00 Reinhard Kahle - Is there a "Hilbert thesis"?
15:00-16:00 João Araújo - The logic of using automated reasoning (course, part 3)
16:00-16:30 Coffee break
16:30-17:00 Luiz Carlos Pereira - The Russell‐Prawitz translation and schematic rules
17:00-17:30 José Espírito Santo - Definable logical operations in the proof-theory of classical logic
17:30-18:00 Filipe Casal - Kolmogorov One-way Functions

30 January 2016
09:00-10:00 Ugo Dal Lago - Implicit complexity and the Curry-Howard correspondence (course, part 3)
10:00-10:30 Coffee break
10:30-11:00 Sérgio Marcelino - Fibred logics: characterizing mixed reasoning and applications
11:00-11:30 Luís Pinto - A coinductive approach to analysis of proof search
11:30-12:30 Hugo Herbelin - A proof with side effects of Gödel's completeness theorem (course, part 3)

Keynote courses by three invited speakers (3 hours each):

• João Araújo (Universidade Aberta, Portugal)
  The logic of using automated reasoning

  Many ask: "Is there any mathematical problem that has been solved using automated reasoning?" The goal of this course is to provide a full, detailed, complete answer to this frequent question. I hope by the end of the course everyone will know that many problems have been solved, and also that automated reasoning is an extremelly helpful tool for the working mathematician.

• Hugo Herbelin (Institut National de Recherche en Informatique et en Automatique, France)
  A proof with side effects of Gödel's completeness theorem

  In the context of the proof-as-program correspondence, classical reasoning is a computational effect which can be interpreted within intuitionistic logic via a negative translation whose computational counterpart is a continuation-passing style translation. We shall consider another computational effect, namely monotonic memory update, which we shall connect to the Kripke's forcing translation. We shall then relate completeness of classical logic with respect to two-valued models to completeness of intuitionistic logic with respect to Kripke models and show that the latter can be seen as a formulation of the former througha a Kripke forcing translation. Going the way back and interpreting Kripke forcing as a memory update, this provides with a proof with side effect of Gödel's completeness theorem whose computational content, when interpreted in a constructive meta-logic, is, like it is generally already the case for completeness of intuitionistic logic, basically replicates the structure of a proof of classical validity into a proof of classical provability.

• Ugo Dal Lago (Università degli Studi di Bologna, Italy)
  Implicit complexity and the Curry-Howard correspondence

  The Curry-Howard Correspondence tells us that proofs behave as programs and formulas act as types. This enabled in the last fifty years a lot of interaction between proof theory and theoretical computer science. Implicit computational complexity, on the other hand, looks for characterizations of complexity classes from programming language theory and mathematical logic. This course starts with a brief overview of the two disciplines, then showing how they have fruitfully interacted in the last thirty years. Some time will be spent, in particular, in describing how techniques from Girard's linear logic can be applied in this context.