We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.

In this paper, we define a realizability semantics for the simply typed $lambdamu$-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.

In this paper, we present the -calculus which at the typed level corresponds to the full classical propositional natural deduction system. The Church–Rosser property of this system is proved using the standardisation and the finiteness developments theorem. We also define the leftmost reduction and prove that it is a winning strategy.