Focalisation and classical realisability

Abstract We develop a polarised variant of Curien and Herbelin’s λ̄µµ ̃ calculus suitable for sequent calculi that admit a focalising cut elimination (i.e. whose proofs are focalised when cut-free), such as Girard’s classical logic LC or linear logic. This gives a setting in which Krivine’s clas-sical realisability extends naturally (in particular to call-by-value), with a presentation in terms of orthogonality. We give examples of applications to the theory of program-ming languages. In this version extended with appendices, we in partic-ular give the two-sided formulation of classical logic with the involutive classical negation. We also show that there is, in classical realisability, a notion of internal complete