KAIST Discrete Math Seminar

The Curry–Howard correspondence says that there is an isomorphic relation between intuitionistic logic and a constructive type theory. The basic idea is that intuitionistic proofs of mathematical formulas contain constructive information to prove them and that the information can be represented as concrete terms in a constructive type theory. One can then use these information and terms to extract computer programs from proofs. The resulting programs are error-free and correct in the sense that they satisfy the prescribed specifications. That means it is certified that the programs work as expected. This talk will explain the basic idea of Curry-Howard correspondence and its use in extracting certified programs.