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.