Title: The proof theoretic foundation of computational logic

Lecturer: Dale Miller

Period: April 10-16, Seminari Est, 11-13

I will present proof theory in the Gentzen/Girard tradition and layer on it recent results on focused proof systems.  I will then make systematic use of that framework to present
  (1) flexible proof systems for classical, intuitionistic, and linear logics;
  (2) a foundation of a range of computational logic tools, ranging from logic programming, theorem proving, and model checking; and
  (3) recent work on defining a general approach to proof certificates.