Realisability semantics of abstract focussing, formalised

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 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.