Logical Foundations of Two-Sided Type Theory
arXiv:2607.14325
The paper develops the logical basis of two‑sided type systems, introducing new systems (2λInt, 2λInt~ and 2λHOL) that correspond to bilateral logic and its extension with strong negation, and proves their consistency and expressive properties.
Abstract
Two-sided type systems, introduced in POPL'24, are an extension of the traditional notion of type system that allows for stating and deriving typing judgements in which (a) assumptions can be made about the types of arbitrary terms and not only variables, and (b) conclusions can be made about any number of type assignments, and not exactly one. In this work, we investigate the logical foundations of two-sided type systems in the sense of the propositions-as-types paradigm. We introduce new two-sided type systems 2Int and 2Int that correspond with Wansing's bilateral logic 2Int and its extension with Nelson's strong negation respectively. Going beyond the propositional case, we introduce 2HOL as an extension of Guevers' HOL, and we show its expressive adequacy, its consistency and that it satisfies both the existence property and its dual.
81 pages