Kripke models for classical logic

We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the meaning of the new notion and its applications to call-by-name proof normalisation. Key words: Kripke model, classical logic, sequent calculus, lambda mu calculus, classical realizability, normalization by evaluation 2000 MSC: 03F99, 03H05, 03B30, 03B40

• Type: Journal
• Year: 2010
• Where: APAL
• Authors: Danko Ilik, Gyesik Lee, Hugo Herbelin
• Keywords: APAL 2010, Classical Logic, Cut-free Completeness, Kripke Model