Hilbert Bernays Summer School on Logic and Computation 2016

The summer school is addressed at students of mathematics, philosophy, computer science and other subjects that are related to mathematics with basic knowledge in logics. The summer school conveys insight into current research topics in the areas of logics and computability. The scientific program consists of mini courses (with lectures, exercises and projects) that are complemented with a historical excursus.


  • From Hilbert to Gentzen and beyond (Reinhard Kahle, Lisbon)
    In this course, both the mathematical and the philosophical ideas behind Hilbert's programme are introduced. Then it will be explained how Gentzen developed modern proof theory from Gödel's results. Finally, contemporary questions about mathematical and philosophical aspects of proof theory are discussed.

  • Proof mining (Ulrich Kohlenbach, Darmstadt)
    In the 1950's Georg Kreisel suggested to apply proof-theoretic transformations to concrete (ineffective) proofs in order to gain additional (new) information. In recent years this approach has successfully been applied to nonlinear analysis. Typically, methods used here are extensions and/or adaptations of Gödel's functional interpretation ("Dialectica interpretation").

  • lambda-calculus (Simona Ronchi della Rocca, Turin)
    Originally developed as logical system, lambda-calculus nowadays serves as base of virtually all functional programming languages. In this course both, the logical background as well as programming techniques are discussed.

  • Computational contents of proofs (Helmut Schwichtenberg, Munich)
    A constructive proof of a formula A can be considered as a solution of the problem given by A. Such a solution is a computable function of a type determined by A. We present a theory of "realisation", based on Gentzen's calculus of natural deduction, and an implemented "proof assistant" which allows to extract computational content from formalized proofs.