Speaker:	Gyesik Lee , ROSAEC Center
Period:	2009-04-10 16:00 ~ 2009-04-10 17:00
Place:	Room 408, Bldg 302, SNU

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.

Short bio

B.S. at the Mathematical Dept. of SNU in 1992,
Master and PhD from the Math. Depof of Univ. of Muenster, Germany.
(Main subject: Mathematical Logic)
Postdoc at the Coq development team of INRIA, France,
and at the Research Center for Information Securiry of AIST, Japan.
From April 2009, Postdoc at ROSAEC Center.

Resources

• talk slide