Sciweavers

APAL
2010

Kripke models for classical logic

13 years 11 months ago
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
Danko Ilik, Gyesik Lee, Hugo Herbelin
Added 08 Dec 2010
Updated 08 Dec 2010
Type Journal
Year 2010
Where APAL
Authors Danko Ilik, Gyesik Lee, Hugo Herbelin
Comments (0)