The proof theory of the constructive modal logic S4 (hereafter $\mathsf{CS4}$ ) has been settled since the beginning of this century by means of either standard natural deduction and sequent calculi or by the reconstruction of modal logic through hypothetical and categorical judgments à la Martin-Löf, an approach carried out by using a special kind of sequents, which keeps two separated contexts representing ordinary and enhanced hypotheses, intuitively interpreted as true and valid assumptions. These so-called dual-context sequents, originated in linear logic, are used to define a natural deduction system handling judgments of validity, truth, and possibility, resulting in a formalism equivalent to an axiomatic system for $\mathsf{CS4}$ . However, this proof-theoretical study of $\mathsf{CS4}$ lacks, to the best of our knowledge, its third fundamental constituent, namely a sequent calculus. In this paper, we define such a dual-context formalism, called ${\bf DG_{CS4}}$ , and provide detailed proofs of the admissibility for the ordinary cut rule as well as the elimination of a second cut rule, which manipulates enhanced hypotheses. Furthermore, we make available a formal verification of the equivalence of this proposal with the previously defined axiomatic and dual-context natural deduction systems for $\mathsf{CS4}$ , using the Coq proof-assistant.

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL’s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories.

This work extends a rule-based specification of nominal C-unification formalised in Coq to include ‘protected variables’ that cannot be instantiated during the unification process. By introducing protected variables, we are able to reuse the C-unification simplification rules to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view, this extension is sufficient to obtain a generalised C-unification procedure; however, it cannot be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification of the inference rules and reuse previous formalisations. We also generalise a functional recursive nominal C-unification algorithm specified in PVS with protected variables, effectively adapting this algorithm to the tasks of nominal C-matching and nominal equality check. The PVS formalisation is applied to test the correctness of a Python manual implementation of the algorithm.