Proceedings Eighth Workshop on Intersection Types and Related Systems
本卷包含在2016年6月26日在波尔图举行的第八届交叉口类型和相关系统研讨会（ITRS 2016）上提交的论文的最终和修订选择，与FSCD 2016合作。
2017-03-30 cs.LO cs.PL
Proceedings Fifth Workshop on Intersection Types and Related Systems
本卷包含第五届交叉口类型和相关系统国际研讨会（ITRS 2010）的会议记录。该研讨会于2010年7月9日在苏格兰爱丁堡举行，作为FLoC 2010的一部分，并与LICS 2010相关联。ITRS研讨会系列旨在汇集研究人员，研究基于交叉口类型和相关方法的系统的理论和实际应用（例如，联合类型、细化类型、行为类型）。
2011-01-21 cs.LO cs.PL
Proceedings Sixth Workshop on Intersection Types and Related Systems
本卷包含第六届交叉口类型和相关系统研讨会（ITRS 2012）的会议记录。该研讨会于2012年6月29日在杜布罗夫尼克（克罗地亚）举行，隶属于第二十七届年度ACM/IEEE计算机科学逻辑研讨会（LICS 2012）。ITRS研讨会旨在汇集研究人员，研究基于交叉口类型和相关方法的系统的理论和实际应用（例如，联合类型、细化类型、行为类型、递归类型等等）。
2013-07-30 cs.LO cs.PL
Programming with union, intersection, and negation types
本文阐述了集合论类型（联合、交集、否定）在编程中的优势，通过语义子类型理论及其扩展，提出并实现了三种有效的语言系统限制，以精确支持分支、模式匹配和函数重载等语言构造的类型化。
2024-03-27 cs.PL
Gradual Liquid Type Inference
液态类型提供了一种可判定的细化推理机制，它很方便，但有两个主要问题：（1）推理是全局的，需要顶级注释，这使得它不适合模块化代码组件的推理，并禁止其适用于库代码，以及（2）推理失败导致模糊的错误消息。这些困难严重阻碍了现有代码的迁移以使用改进。本文表明，逐步液体类型推断-液体推理和逐步细化类型的新组合-解决这两个问题。支持乐观解释的不精确谓词的渐进细化类型可以在参数位置中使用以约束流动推理，使得全局推理过程e有效地推断可用于库组件的模块化规范。双重地，当逐渐改进作为推理的结果出现时，它们表示静态改进的使用不一致。因为液体细化是从一个nite集合的谓词，在逐渐液体类型推断，我们可以枚举每个不精确的细化的安全具体化，即静态细化，证明为什么一个程序是逐渐良好的类型。此枚举对于静态液体类型错误的解释非常有用，因为安全具体化显示了导致静态类型错误的所有潜在不一致性。我们发展了渐进式液态类型推断理论，并在液态Haskell语言环境下对其语用进行了探讨。
2019-10-30 cs.PL
A Finite Model Property for Intersection Types
我们表明，被称为BCD的交集类型的关系理论具有有限模型属性，即BCD是完全的有限模型。我们的证明使用重写技术，作为一个直接的副产品的多项式时间的可判定性的前序<=（虽然这也遵循所谓的β健全的BCD）。
2015-03-17 cs.LO cs.PL
Intersections and Unions of Session Types
先前的工作已经扩展了线性递归演算和会话类型的消息传递并发计算之间的深层逻辑联系，具有等递归类型和子类型的自然概念。在本文中，我们进一步扩展了交集和联合类型，以表示在一个单一的类型过程的多个行为属性。我们证明了会话的保真度和没有死锁，并说明了我们的系统的表达能力与一些简单的例子。我们观察到，我们可以表示内部和外部的选择的交集和工会，分别，这是以前建议由Padovani为不同的语言的会话类型的动机是操作，而不是逻辑问题。
2017-02-08 cs.LO cs.PL
Intersection types for unbind and rebind
我们定义了一个类型系统的交集类型的扩展的Unbind和rebind操作符的Adjuda演算。在这个演算中，一个带有自由变量的术语，代表开放代码，可以打包成一个“未绑定”术语，并作为一个值传递。为了在代码内部执行，未绑定项应该在使用它的地方显式地重新绑定。Unbinding和rebinding是分层的，也就是说，术语可以包含任意嵌套的未绑定术语，其内部代码只能在应用了一系列rebinds之后执行。相应地，类型用级别装饰，如果一个项需要k次重新绑定才能还原为一个值，则它的类型用k装饰。通过交集类型，我们模拟了一个事实，即一个术语可以在提供不同数量的解绑的上下文中以不同的方式使用。特别地，顶级术语，即不需要解绑来还原为值的术语，应该具有值类型，即至少一个元素具有级别0的交集类型。与建议的交叉类型的系统，我们得到的按值调用的策略下，这是以前的类型系统没有解决的问题的合理性。
2011-01-24 cs.LO cs.PL
Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices
带有de Bruijn索引的Alzida演算将Alzida项的每个alpha类集合到一个唯一项中，使用索引而不是变量名。交集类型提供有限类型多态性，并且可以通过当且仅当一个项是可类型化的时才可规范化的属性来规范化可规范化的交集项。为了更接近计算，并简化beta压缩中原子操作的形式化，几个显式替换演算主要是用de Bruijn指数开发的。没有类型和简单类型系统的显式替换演算的版本与更复杂的类型系统（如交集类型）的版本相比，得到了很好的研究。在以前的工作中，我们介绍了一个de Bruijn版本的交叉类型系统的Adjuda演算，并证明了它保持主题约简，类型系统的基本属性。本文提出了一个具有de Bruijn指标的交型系统，它最初被引入到Beta-范式的主类型化中。我们提出了在这个新的系统和相应的版本的类型推断和重建的范式从主要类型算法的特点。我们简要讨论了主体归约性质的失效和可能的解决方案。
2010-01-25 cs.LO cs.PL
Proceedings Seventh Workshop on Intersection Types and Related Systems
本卷包含了最终的和修订的论文选择在第七次研讨会上提出的交叉类型和相关系统（ITRS 2014），在维也纳（奥地利）举行的7月18日，附属于TLCA 2014，类型λ演算和应用（与RTA，重写技术和应用联合举行）作为FLoC和维也纳逻辑夏季（VSL）2014的一部分。交集类型在20世纪70年代末被引入，作为描述λ演算的属性的语言，这些属性没有被所有以前的类型系统捕获。它们提供了强规范化lambda项的第一个特征，并已成为分析各种规范化属性以及lambda模型的强大语法和语义工具。近年来，交叉口类型的研究范围不断扩大。最近，在将交集类型和类似技术用于诸如程序分析、验证和并发以及程序合成的实际目的方面已经有了许多突破。ITRS研讨会系列的目的是汇集研究人员，研究基于交叉口类型和相关方法的系统的理论和实际应用（例如，联合类型、细化类型、行为类型）。
2015-03-15 cs.LO cs.PL cs.SE
Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems
本卷包含在计算模型发展第十二次研讨会（DCM 2018）和交叉口类型和相关系统第九次研讨会（ITRS 2018）上提交的论文的最终和修订选择，于2018年7月8日在牛津举行，与FLOC 2018合作。
2019-04-21 cs.CC cs.LO cs.PL
Uniform Proofs of Normalisation and Approximation for Intersection Types
我们提出了交叉型系统的风格的微积分，修改的系统，瓦伦蒂尼介绍了证明规范化属性，而不使用reductionmethod。我们的系统比Valentini的系统更自然，相当于通常的自然演绎风格的系统。我们证明的特征定理的强和弱规范化，通过建议的系统，而且，通过直接的归纳论点的近似定理。这提供了一个统一的方式证明的规范化和近似定理通过类型系统在微积分风格。
2015-03-17 cs.LO cs.PL
Intersection Types for a Computational Lambda-Calculus with Global State
本文研究带全局存储读写操作的无类型 lambda 演算，利用 monad 建模副作用，建立操作语义、指称语义与交集类型系统，并证明类型不变性及收敛项的类型刻画。
2025-08-27 cs.LO cs.PL
Transitivity of Subtyping for Intersection Types
交叉类型的子类型规则传统上采用传递性规则（Barendregt et al. 1983），这意味着子类型不满足子公式属性，使得它更难以用于编译器验证的过滤器模型。Laurent开发了一个序列风格的子类型系统，没有传递性，并通过一系列六个引理证明了传递性，最终在切割消除（2018）。本文开发了一个规则风格的子类型系统，省略了传递性，并提供了传递性的直接证明，显着减少了证明的长度，将六个引理交换为一个引理。受Laurent系统的启发，函数类型的规则本质上是$β$可靠性。新系统满足“子公式合取性质”：在$A <: B$的推导中出现的每一个类型都是$A$或$B$的子公式，或者是这些子公式的交集。本文证明了新的亚型系统与Barendregt、Coppo和Dezani-Ciancaglini的亚型系统是等价的。
2020-05-15 cs.LO cs.PL
Monadic Intersection Types, Relationally (Extended Version)
本文将交类型扩展到带代数效应的计算性 λ-演算，提出单子交类型系统，并结合句法技术与抽象关系推理刻画程序与环境在有限及无限设定下的可观察交互行为。
2024-01-23 cs.LO cs.PL
Linearising Explicit Substitutions using Intersection Types
LIACC；Faculdade de Ciências, Universidade do Porto（波尔图大学理学院）；CRACS, INESC-TEC（CRACS，INESC-TEC）
研究为带显式替换的演算定义新项展开，以此关联带显式替换的lambda演算与Boudol的带多重性的资源感知lambda演算，函数参数可用性或受限，核心方法是新项展开，主要贡献是建立了这种关联。
2026-07-23 cs.LO cs.PL
Typing Classes and Mixins with Intersection Types
我们研究了一个具有记录和记录合并算子的代数演算的交集类型赋值系统，其中类型在主题缩减和扩展下都保持不变。演算的表达能力足以自然地将mixin表示为递归定义的类上的函数，类的固定点（对象）是递归记录。尽管定义中涉及到双重递归，但类和mixin可以有意义地类型化，而无需求助于递归或F有界多态类型。然后，我们将mixin构造和组合适应于Java和C#，仅依赖于现有的功能，从而使生成的代码在各自的类型系统中保持可类型化。我们展示了一些示例代码，并研究其在交叉类型系统中的类型，通过解释到我们所提出的记录的代数演算。
2015-03-17 cs.LO cs.PL cs.SE
Hybrid Intersection Types for PCF (Extended Version)
本文提出了一种针对PCF的可靠且完备的定量交集类型系统PCFH，首次使传名调用和传值调用的操作行为在混合计算模型中共存，并提供归约序列长度的精确上界。
2024-04-22 cs.LO cs.PL
Sequence Types and Infinitary Semantics
我们引入了一个新的表示非幂等交集类型，使用\textbf{sequences}（家庭索引的自然数），而不是列表或多集。这允许将\textbf{intersection type}理论扩展到无限$λ$ -演算。因此，我们的特点是遗传头部正常化，这给出了一个积极的答案，被称为\textbf{Klop's Problem}的问题。在我们的方法中，我们使用\textbf{non-idempotent intersection}检索一些著名的结果无穷项。
2021-12-15 cs.LO cs.PL
Lucretia - intersection type polymorphism for scripting languages
从长远来看，脚本代码可能会带来维护问题。因此，需要一种方法，使以自动方式控制用动态语言编写的程序的属性成为可能。我们介绍了Lucretia，一种具有内省原语的核心语言。Lucretia配备了一个（改进的）静态类型系统，该系统基于描述所使用对象结构的类型的本地更新。通过这种方式，我们处理脚本语言最动态的特性之一，即对象接口的运行时修改。在我们的系统中，判断有一个类似霍尔的形状，因为它们有一个先决条件和一个后置条件部分。前置条件描述了在某个表达式执行之前可见对象的接口的静态近似，后置条件描述了表达式执行之后的接口。字段更新操作使系统中的混叠问题复杂化。我们通过在方法签名中引入交集类型来应对它。
2015-03-17 cs.LO cs.PL
Resolution as Intersection Subtyping via Modus Ponens
解析和子类型化是程序设计语言中两种常见的机制。Resolution由诸如类型类或Scala风格的implant之类的功能使用，以自动从上下文类型信息合成值。子类型通常用于将值的类型自动转换为另一个兼容的类型。到目前为止，这两种机制一直被认为是相互独立的。本文表明，一个小的扩展，子类型与交叉类型可以substrate分辨率。这有三个主要后果。第一，解决不需要作为一个单独的机制来实施。其次，解析和子类型化之间的相互作用变得明显。最后，将解析集成到子类型中可以实现一流（隐式）环境。通过子类型恢复归结能力的扩展是命题逻辑的肯定前件规则。虽然它很容易添加到声明子类型中，但需要非常小心地保留所需的属性，例如算法子类型的传递性和可判定性以及一致性。为了实现这些想法，我们开发了$λ_i^{\mathsf{MP}}$，一个演算，扩展了iperrival演算与不相交的交集类型，并在Coq定理证明器中开发其元理论。
2020-10-15 cs.LO cs.PL
A Type Checker for a Logical Framework with Union and Intersection Types
我们提出的语法，语义和类型规则的公牛，一个原型定理证明的基础上的三角洲框架，即一个完全类型化的Alkida演算装饰与工会和交叉类型，如作者在以前的论文中所描述的。Bull还实现了Barbanera-Dezani-de'Liguoro的类型论Xi的子类型算法。Bull有一个命令行界面，用户可以在其中声明公理，术语，并执行计算和一些基本的终端风格的功能，如错误漂亮打印，子表达式突出显示和文件加载。此外，它可以对证明进行类型检查或规范化，这些项可能是不完整的，因此类型检查算法使用统一来尝试构建缺失的子项。Bull使用Berardi的纯类型系统的语法来提高内核的紧凑性和模块性。抽象语法和具体语法基本上是一致的，并且与Coq的具体语法相似。Bull对术语使用高阶统一算法，而类型检查和部分类型推断是通过双向细化算法完成的，类似于Matita和Beluga中发现的算法。精化可以分为两个部分：本质精化和类型精化。绑定器使用常用的de Bruijn索引实现。我们已经定义了一个具体的语言语法，允许用户编写Delta-terms。我们已经定义了约简规则和评价器。我们从头开始实现了一个细化器，它可以进行部分类型检查和类型重构。我们已经实验了公牛经典的例子的交集和工会的文学，如形式化的Pfenning与他的细化类型在LF。我们希望，这种研究静脉可能是有用的实验，在证明理论的设置，形式的多态性替代吉拉德的参数…
2020-02-25 cs.LO cs.PL
