Realisability semantics of abstract focussing, formalised
St\'ephane Graham-Lengrand (CNRS - Ecole Polytechnique - INRIA - SRI, International)

TL;DR
This paper develops a parametrized sequent calculus for abstract focussing with proof-terms, capturing both classical and intuitionistic variants, and establishes a realisability semantics formalised in Coq, including an adequacy proof.
Contribution
It introduces a flexible framework for abstract focussing with proof-terms and provides a higher-level realisability semantics formalised in Coq, unifying classical and intuitionistic systems.
Findings
Proves the Adequacy Lemma for the system's semantics.
Formalises the entire system and semantics in Coq.
Shows the semantics reflect Zeilberger's universal quantification.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
