AI 中文总结
研究双边类型系统的逻辑基础，引入对应万辛双边逻辑及扩展的新双边类型系统2$\lambda$Int和2$\lambda$Int$^{\sim}$，还引入2$\lambda$HOL扩展格弗斯的$\lambda$HOL，展示其表达充分性、一致性及相关属性。
AI 中文摘要
在POPL'24中引入的双边类型系统是传统类型系统概念的扩展，允许陈述和推导类型判断，其中（a）可以对任意项的类型进行假设，而不仅仅是变量，（b）可以对任意数量的类型赋值得出结论，而不只是一个。在这项工作中，我们从命题即类型范式的角度研究双边类型系统的逻辑基础。我们引入了新的双边类型系统2$\lambda$Int和2$\lambda$Int$^{\sim}$，它们分别对应于万辛的双边逻辑2Int及其与尼尔森强否定的扩展。超越命题情况，我们引入2$\lambda$HOL作为格弗斯的$\lambda$HOL的扩展，并展示了它的表达充分性、一致性，以及它满足存在性属性及其对偶。
英文摘要
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$λ$Int and 2$λ$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$λ$HOL 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.
Comments81 pages
