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