The opening lecture recalled the historical links between logic and computer science. The 2018-2019 lecture by the Software Science chair explored another link, mathematical in nature (it's an isomorphism), between programming languages and mathematical logics. In this approach, demonstrating a theorem is the same as writing a program ; stating the theorem is the same as specifying the type of program.
This correspondence between demonstration and programming was first observed in a simple case by two logicians : Curry in 1958, then Howard in 1969. The result seemed so anecdotal that Howard never submitted it to a journal, contenting himself with circulating photocopies of his handwritten notes. Rarely has a photocopy had such a scientific impact, so much so that this Curry-Howard correspondence resonated with the revival of logic and the explosion of theoretical computer science in the 1970s, and by 1980 had established itself as a profound structural link between languages and logics, programming and demonstration.
Today, it's natural to ask what is the " logical meaning " of this or that programming language feature, or what is the " computational content " of this or that mathematical theorem (i.e., what algorithms are hidden in its demonstration ?). Most importantly, the Curry-Howard correspondence has led to computer tools such as Coq and Agda, which are both programming languages and mathematical logics, and are used to write and verify programs as well as to state and help demonstrate mathematical theories.
The lecture traced this ferment of ideas at the frontier between logic and computer science, and focused on recent results and open problems in the field. The seminar featured contributions from seven experts in the field, providing further insights and complementary points of view.