Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper explores the logical foundations of two-sided type systems, extending traditional type theory to allow assumptions about arbitrary terms and conclusions about multiple type assignments. The authors introduce new systems, 2λInt and 2λInt∼, which align with established bilateral logic frameworks, and further develop 2λHOL as an extension of λHOL. Key results include demonstrating expressive adequacy, consistency, and the satisfaction of both the existence property and its dual for these systems.
Two-sided type systems can express complex typing judgements that traditional systems cannot, fundamentally altering our approach to type theory.
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 2$\lambda$Int and 2$\lambda$Int$^{\sim}$ that correspond with Wansing's bilateral logic 2Int and its extension with Nelson's strong negation respectively. Going beyond the propositional case, we introduce 2$\lambda$HOL as an extension of Guevers'$\lambda$HOL, and we show its expressive adequacy, its consistency and that it satisfies both the existence property and its dual.