Relationship between Curry-Howard-correspondence and semantics Seminars/Workshops

Abstract

Curry-Howard-correspondence establishes a correspondence between proofs and programs. That is, we can extract a correct program from a proof of its specification. Furthermore, it is well known that it is easier to prove the correctness of a program if one derives the program from its specification rather than first writing the program and then proving the correctness. In this talk, we introduce how to use semantic elements, like the completeness proof for (classical or intuitionistic) first order logic w.r.t. Kripke model-style forcing relation, to get a certified program from a proof.