Sciweavers

CSL
2009
Springer
13 years 11 months ago
Focalisation and Classical Realisability
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 ...
Guillaume Munch-Maccagnoni