Realisability semantics of abstract focussing, formalised

Stéphane Graham-Lengrand
(CNRS - Ecole Polytechnique - INRIA - SRI International)

We present a sequent calculus for abstract focussing, equipped with proof-terms: in the tradition of Zeilberger's work, logical connectives and their introduction rules are left as a parameter of the system, which collapses the synchronous and asynchronous phases of focussing as macro rules. We go further by leaving as a parameter the operation that extends a context of hypotheses with new ones, which allows us to capture both classical and intuitionistic focussed sequent calculi. We then define the realisability semantics of (the proofs of) the system, on the basis of Munch-Maccagnoni's orthogonality models for the classical focussed sequent calculus, but now operating at the higher level of abstraction mentioned above. We prove, at that level, the Adequacy Lemma, namely that if a term is of type A, then in the model its denotation is in the (set-theoretic) interpretation of A. This exhibits the fact that the universal quantification involved when taking the orthogonal of a set, reflects in the semantics Zeilberger's universal quantification in the macro rule for the asynchronous phase. The system and its semantics are all formalised in Coq.

In Iliano Cervesato and Carsten Schürmann: Proceedings First International Workshop on Focusing (WoF'15), Suva, Fiji, 23rd November 2015, Electronic Proceedings in Theoretical Computer Science 197, pp. 15–28.
Published: 8th November 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.197.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org