Curry-Howard correspondence (formulae-as-types, proofs-as-programs) is a highly popular observation about the close connection between foundations of mathematics and computer science. Having appeared in the middle of the last century, it triggered an explosion of various interpretations, applications, and generalizations, which is still actively ongoing. The expansion goes in two directions: more and more logical and computational systems become interconnected, and also new dimensions are added to the correspondence, lengthening the name of the fact (so for the sake of completeness nowadays we should rather talk about the Curry-Howard-Lambek-Scott-Tarski-Stone-Voevodsky correspondence, but we will refrain from this and confine our discussion to the first three surnames).
In the first part of the talk, we will discuss the famous correspondence, in particular its categorical side. In the second part, we will consider one specific application -- to logic programming -- and in addition will get acquainted with the concept of uniform proofs -- the foundation of logic programming languages.
Presenter: Dmitrii Rozplokhas
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg
State University, Stary Peterhof, Universitetski pr., 28