Intersection Types and Lambda Theories
我们说明了使用交叉类型作为一个语义工具，显示属性的lambda理论的晶格。依靠易交类型论的概念，我们成功地建立了一个过滤器模型，其中任意简单易项的解释是任何过滤器，可以用一个谓词以统一的方式描述。这使我们能够证明一个众所周知的lambda理论的一致性：这种一致性对lambda理论格的代数结构有着有趣的影响。
2002-11-12 cs.LO
Intersection Types for Unboundedness Problems
交集类型最初是作为简单类型的扩展开发的，但它们也可以用于细化简单类型。在本调查中，我们集中在后一种选择;更确切地说，在使用交集类型来描述简单类型的交集项的定量属性。我们提出了两种类型的系统。第一个允许估计（通过适当定义的值的推导）的固定常数“a”的出现在考虑的β-范式的一个考虑的非线性项的数量。第二种类型的系统更复杂，并且允许估计常数'a'在单个分支上出现的最大次数。
2019-04-23 cs.LO
Inhabitation for Non-idempotent Intersection Types
本文研究了非幂等交集类型的居留问题，针对刻画可解或强规范化lambda项的系统，提供了可靠且完备的算法，证明了其可判定性。
2018-08-02 cs.LO
Natural Deduction and Normalization Proofs for the Intersection Type Discipline
改进和扩展以前的工作Retoré，我们开发了一个系统的方法，通过自然演绎的交叉类型。我们展示了如何一个步骤的β减少可以被看作是执行，在一级的类型推导，Prawitz减少并行。然后，我们推导出作为直接后果的主题减少的主要定理规范化的交集类型：系统D，强规范化，系统欧米茄，最左边的减少终止的条款类型没有欧米茄。
2019-04-23 cs.LO
Intersection Subtyping with Constructors
我们研究了用额外的类型构造函数扩展BCD交叉类型系统的问题。在类型方面，我们专注于为产品类型添加通常的规则。在子类型方面，我们考虑一种通用的方法来定义一个子类型的关系，家庭的类型，其中包括交叉类型。我们通过考虑类型构造函数是交集、欧米茄和箭头的特殊情况，找到了BCD子类型关系。作为另一个实例，我们得到了BCD子类型到产品类型的扩展。我们展示了如何保存类型的减少和扩大是满意的，在所有考虑的情况下。我们的方法受益于“子公式属性”的子类型关系的建议介绍。
2019-04-23 cs.LO
The Algebraic Intersection Type Unification Problem
本文证明代数交集类型合一问题是指数时间困难的，即使在秩1解下也成立，并给出交集类型匹配的固定参数不可解性结果，采用博弈论方法获得首个非平凡下界。
2017-08-14 cs.LO
Infinitary Intersection Types as Sequences: a New Answer to Klop's Question
我们提供了一个类型理论的特征弱正规化的条款在无穷大演算。为此，我们适应标准的定量（与非幂等交叉点）类型的分配系统，我们的无穷微积分的Ausada演算。我们的工作为Klop的HHN-问题提供了一个新的答案，即，找出是否存在一个类型系统来表征遗传头归一化（HHN）项。龙田证明了HHN不能用有限类型系统来刻画。我们证明了一个无穷型系统赋予的有效性条件称为逼近可以实现它。
2016-10-20 cs.LO
On sets of terms having a given intersection type
本文在交集类型赋值系统中证明每个强规范化项具有唯一性类型，并探讨类型代数表示，同时证明给定类型的封闭项集合的一致可分离性及无限时的数字系统性质。
2022-09-20 cs.LO
Sensible Intersection Type Theories
Università di Torino（都灵大学）；Kutaisi International University（库塔伊西国际大学）；Tbilisi State University（第比利斯国立大学）；Università del Piemonte Orientale（皮埃蒙特东部大学）；Università di Udine（乌迪内大学）
本文研究了交类型理论中有意义滤波模型的构造与性质，提出通过meet-semilattices和态射保持有意义性，并推广Mendler准则到交类型和头部归约项。
2026-03-04 cs.LO
Mixin Composition Synthesis based on Intersection Types
提出基于交集类型类型居留的mixin组合合成方法，通过类型转换与仓库构建，实现类与mixin组合的自动合成。
2018-02-26 cs.LO
Reduction in X does not agree with Intersection and Union Types (Extended abstract)
本文定义了演算X的交集和并集类型赋值，X是一种与经典逻辑的根森演算具有Curry-Howard对应关系的替换自由语言。我们表明，这个概念是封闭的主语扩展，并表明，它需要加以限制，以满足主语减少以及，使其不适合定义的语义。
2011-09-21 cs.LO
Toward Isomorphism of Intersection and Union types
本文研究了具有交和并类型的代数演算的类型同构。众所周知，在微积分中，两种类型之间的同构是由一对相互逆的项实现的。值得注意的是，可逆项是特定形状的线性项，称为有限遗传置换子。然后，在线性项的交、并类型的相关类型推断系统中，研究了有限遗传置换子的类型性质。特别地，定义了类型之间的同构保持约简。类型归约是汇合的和终止的，并引入了类型的范式的概念。正规类型的性质是完全刻画类型同构的关键一步。本文的主要结果是，一方面证明了具有相同范式的两个类型是同构的，另一方面证明了在范式中两个类型之间同构的特征，箭型的模同构。
2013-07-31 cs.LO
Factoring Derivation Spaces via Intersection Types (Extended Version)
在典型的非幂等交集型系统中，证明规范化是不融合的。本文引入了一个合流非幂等交型系统。类型推导使用证明项语法。该系统具有良好的性能：主题减少，强规范化，和一个非常正规的残差理论。通过模拟定理建立了与微积分的对应关系。非幂等交集类型的机制允许我们跟踪获得答案所需的资源的使用情况。特别是，它引入了垃圾的概念：如果计算对获得答案没有贡献，那么它就是垃圾。使用这些概念，我们表明，一个的派生空间的一个ESTA项可以因式分解使用的Grothendieck建设半格的一个变种。这意味着，特别是，任何推导在Aidda演算可以被唯一地写为一个无垃圾前缀后跟垃圾。
2019-07-20 cs.LO
A Complete Characterization of Complete Intersection-Type Theories
我们描述了这些交集类型论，产生完整的交集型分配系统的代数演算，相对于三个典型的集合理论的交集型语义：推理语义，简单语义和F-语义。这些语义的产生是通过将可应用结构的类型子集的解释，作为交集构造函数集合论包含的解释，以及将箭头构造函数a 'la Scott的解释，关于任何可能的功能集，或最大的一个，或最小的一个。这些结果加强和推广显着所有早期的结果在文献中，据我们所知，在至少三个方面。首先，推理语义在以前没有被考虑过。其次，这些刻画都是根据类型上的前序关系的简单闭包条件给出的，而不是根据类型判断本身给出的。因此，检查条件的任务变得相当容易处理。最后，我们并不局限于注意力仅仅是一个解释模型，但任意的应用结构，承认一个解释功能。因此，我们也允许治疗模型的限制性肾结石。尽管如此，我们给出的特征可以仅适用于非线性模型的情况。
2000-11-23 cs.LO
On Isomorphism of "Functional" Intersection and Union Types
类型同构对于检索库组件很有用，因为库中的函数可以具有与用户期望的类型不同但同构的类型。此外，类型同构免费提供了在用户程序中包含正确类型的函数所需的强制。本文研究了具有交类型和并类型的系统的类型同构问题。在交和并的存在下，同构不是一个同余，不能用等式的方式来描述。仍然可以给出一个特征，但由于函数类型和非函数类型之间的干扰而变得非常复杂。在本文中，我们将每个原子类型解释为将任何参数映射到类型本身的解释中的函数集，从而面临这个缺点。这一选择是由斯科特的逆极限模型的初始投影提出的。本文的主要结果是保证型同构的条件，基于同构保持约简。
2015-03-17 cs.LO
The Delta-calculus: syntax and types
我们提出了Delta演算，一个显式类型的Delta-calculus强对，投影和显式类型的Delta-calculus。演算可以用不同的交集类型论T参数化，例如Coppo-Dezani、Coppo-Dezani-Salle '、Coppo-Dezani-Venneri和Barendregt-Coppo-Dezani理论，产生具有相关交集类型系统的Delta-演算族。我们证明了它的主要性质，如Church-Rosser，类型唯一性，主题约简，强规范化，类型检查和类型重构的可判定性。本文通过一个将显式Delta项转换为纯Delta项的本质函数，说明了Curry型交集型赋值系统与Church型交集型赋值系统之间的关系.最后，我们将一个带类型子的Delta项翻译成一个不带类型子的Delta项，证明了这种翻译是连贯的，因为它的本质是恒等式。一般的Delta演算可以被参数化，以考虑其他的交集类型论，如Barendregt等人的书中的理论。
2019-02-25 cs.LO
Characterisation of Approximation and (Head) Normalisation for $λμ$ using Strict Intersection Types
我们研究了[van Bakel'16]中提出的严格类型分配。我们定义了一个概念的近似的dumda-mu-terms，表明它产生的语义，并为每个类型的长期有一个近似，具有相同的类型。我们表明，这导致通过分配类型的所有条款，有一个头范式的一个特征，并为所有条款，有一个范式，以及一个为所有条款的强规范化。
2017-02-08 cs.LO
Intersection Types for the Computational lambda-Calculus
我们研究多态类型分配系统的非类型的的影响，基于Moggi的单子方法。从单子的抽象定义出发，我们引入了一个基于Wadler的变体的按值调用的计算型微积分，该变体具有单元和绑定组合子，并且没有let。我们定义了一个概念，减少演算，并证明它是合流的，我们也涉及到我们的演算的原始工作的莫吉表明，他的无类型的元语言可以解释和模拟在我们的演算。然后，我们介绍了一个交集型系统启发Barendregt，Coppo和Dezani系统的普通λ演算，建立转换下的类型不变性，并通过逆极限和过滤器模型的构造提供了演算的模型，并将它们联系起来。我们证明了类型系统的可靠性和完备性，以及主题缩减和扩展属性。最后，我们引入了一个收敛的概念，这是完全相关的减少，并通过其类型的收敛项的特征。
2020-02-07 cs.LO
Intersection Types for the lambda-mu Calculus
我们介绍了一个交叉型系统的的Yuda-mu演算是不变的主题减少和扩展。该系统是通过描述Streicher和Reus的指称模型的连续的范畴内的欧米茄代数格通过Abramsky的域逻辑方法。这同时提供了类型系统的解释，并通过过滤器模型构造证明了系统相对于连续模型的完备性。然后，我们定义了我们的系统的限制，这样的一个denda-mu项是可类型的，当且仅当它是强规范化的。我们还表明，Parigot的typing与经典有效的命题公式，Muda-mu条款可以被翻译到限制系统，然后提供了一个替代的证明强规范化的类型Muda-mu演算。
2018-01-09 cs.LO
Uniqueness typing for intersection types
在Coppo，Dezani-Ciancaglini和Veneri [1981]的交叉类型分配系统的变体中，我们证明了关于具有给定交叉类型的项集的几个事实。我们的主要结果是：每一个强正规化项$M$都有一个 * 唯一型 *，它是一个$(Γ,A)$对，使得1）$Γ\vdash M : A$ 2）$Γ\vdash N : A \Longrightarrow M =_{βη} N$我们还讨论了交型代数的几种表示，以及相应的类型分配规则的选择.
2021-05-09 cs.LO math.LO
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
Strong normalization through idempotent intersection types: a new syntactical approach
Università di Torino（都灵大学）；CONICET—Universidad de Buenos Aires（阿根廷国家科学研究委员会—布宜诺斯艾利斯大学）；Universidad Nacional de Quilmes（基尔梅斯国立大学）
本文提出了一种基于幂等交集类型的语法方法，通过度量证明强规范性，扩展到两种交集类型系统。
2026-02-27 cs.LO
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
Intersection Types and Counting
我们提出了一种新的方法来解决以下元问题：给定树的一个数量属性，设计一个类型系统，使得由无限基元项生成的树的期望属性对应于该元项的类型的导出的一些属性，在这个类型系统中。我们的方法是在特殊情况下的语言有限性问题的非确定性高阶递归计划（HORS）：给定一个非确定性的HORS，决定这HORS生成的所有有限树的集合是否是有限的。我们给出一个类型系统，使得HORS可以生成任意大的有限大小的树当且仅当在类型系统中，我们可以获得任意大的导子，在适当的意义上，后一个条件可以很容易地决定。
2017-03-30 cs.LO
An Indexed Linear Logic for Idempotent Intersection Types (Long version)
引入Indexed Linear Logic的幂等变体，通过基变换重构语法并利用子类型关系实现幂等性，证明其作为逻辑能细化经典线性逻辑且切消过程终止并合流。
2024-02-15 cs.LO
Execution Time of lambda-Terms via Denotational Semantics and Intersection Types
线性逻辑的基于多集的关系模型导出了无类型演算的语义，它对应于一个非幂等交类型系统System R。我们证明了，在系统R中，类型派生的大小和类型的大小是密切相关的执行时间在一个特定的环境机器，Krivine的机器。
2009-05-26 cs.CC cs.LO
Rank 3 Inhabitation of Intersection Types Revisited (Extended Version)
我们重新审视了秩3交集型居住的不可判定性结果（Urzyczyn 2009），以追求两个目标。首先，我们加强了以前的结果，表明交集类型居住是不可判定的秩3和顺序3的类型，即没有必要在证明搜索过程中引入新的函数依赖（新的指令）。其次，我们指出的原则，直接模拟图灵机计算，而以前的建设使用高度并行和非确定性的计算模型。由于我们的构造比现有的方法更简洁，没有走弯路，我们相信这是有价值的，更好地理解的表现力的交叉型居住。
2017-08-21 cs.CC cs.LO
A Finite Model Property for Intersection Types
我们表明，被称为BCD的交集类型的关系理论具有有限模型属性，即BCD是完全的有限模型。我们的证明使用重写技术，作为一个直接的副产品的多项式时间的可判定性的前序<=（虽然这也遵循所谓的β健全的BCD）。
2015-03-17 cs.LO cs.PL
Principal Typing for Intersection Types, Forty-Five Years Later
University of Turin（都灵大学）
本文通过三种基本操作设计半算法，计算强归约项的主类型，为交集类型中的主类型属性提供现代视角。
2026-03-04 cs.LO
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
On Jumps, Interactions, and Intersection Types
Université Sorbonne Paris Nord（索邦巴黎北大学）；Università di Bologna（博洛尼亚大学）；Inria（法国国家信息与自动化研究所）；IRIF, Université Paris Cité（IRIF，巴黎西岱大学）
本文提出参数化跳跃抽象机（PaJAM），并证明其与非幂等交集类型之间的紧密对应，通过类型推导可提取计算步数，且通过限制回溯深度可统一经典模型。
2026-06-26 cs.LO
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
Resource control and intersection types: an intrinsic connection
在本文中，我们研究了$λ$ -演算，一个$λ$ -演算丰富的资源控制。资源的显式控制是通过擦除和复制操作符的存在来实现的，这些操作符对应于类型分配系统中的细化和收缩规则。我们直接引入了$λ$ -项类，并通过将其分解为原子步，给出了一种新的代换处理方法。本文提出了一个$λ$ -演算的交集型赋值系统，它明确了变量的三种角色与三种交集型之间的对应关系。最后，我们通过一个交型赋值系统给出了$λ$ -演算中强正规化的刻画。该过程使用了范式的可类型性、Redex主题扩展和归约方法。
2014-12-06 cs.LO math.LO
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 and (Positive) Almost-Sure Termination
随机化高阶计算可以被看作是被赋予了单个代数运算的λ演算捕获的，即二元概率选择的构造。这种计算的重要性在于获得任何给定结果的概率，而不是获得它的可能性或必要性，就像在（非）确定性计算中一样。终止，可以说是最简单的可达性问题，至少可以用两种方式来解释，这取决于它是谈论收敛的概率还是期望的评估时间，第二个提供了更强的保证。在本文中，我们证明了交集类型能够精确地描述单个类型系统内的两个终止概念：任何λ项的收敛概率都可能被其类型低估，而底层推导的权重给出了项的期望值的下限。步骤到范式。值得注意的是，这两个近似都是紧的--不仅是可靠性，而且是完整性。关键的成分是非幂等性，没有它就不可能推理出完全评估任何项所需的约简步骤的预期数量。此外，我们还从理论上证明了所得到的近似是最优递归：没有递归可逼近的形式系统能比它做得更好。
2020-12-23 cs.LO
A journey through resource control lambda calculi and explicit substitution using intersection types (an account)
在本文中，我们邀请读者通过三个lambda演算与资源控制的旅程：lambda演算，lambda演算和lambda演算与显式替换。由于弱化和收缩运算符的存在，这三种演算都可以显式控制资源。在这个过程中，我们提出了所有三个资源控制演算的交集型分配系统。我们认识到需要三种变量都需要不同类型的交叉点类型。我们的主要贡献是在所有三个结石的减少强规范化的特点，使用的技术reductionary，头部主题扩展，以及订单和适当的嵌入的条款相结合。
2013-06-10 cs.LO math.LO
Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis
我们描述了正在进行的工作，从软件组件库的自动组合合成的框架。这项工作是基于组合逻辑与交叉类型。这个想法是，组件被建模为类型的组合子，和居住的算法{ \textemdash }是否有一个组合项e与类型tau相对于环境伽玛？{ \textemdash }可用于合成组合物。在这里，Gamma以类型化组合子的形式表示存储库，tau指定合成目标，e是合成程序。我们说明我们的方法的例子，包括应用程序的GUI组件合成。
2013-07-31 cs.LO cs.SE
Intersection Types for a Computational Lambda-Calculus with Global State
本文研究带全局存储读写操作的无类型 lambda 演算，利用 monad 建模副作用，建立操作语义、指称语义与交集类型系统，并证明类型不变性及收敛项的类型刻画。
2025-08-27 cs.LO cs.PL
Intersection Types via Finite-Set Declarations
本文提出 f-cube，通过有限集声明将交叉类型编码为 Pi 类型，从而在不使用交叉引入规则的情况下为 lambda-cube 无法赋型的强规范化项 U' 赋予类型。
2024-05-01 cs.LO math.LO
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
Intersection Types and Counting
我们提出了一种新的方法来解决以下元问题：给定树的一个数量属性，设计一个类型系统，使得由无限基$λ$ -项生成的树的所需属性对应于该$λ$ -项的类型的导出的某些属性，在该类型系统中。我们的方法是在特殊情况下的语言有限性问题的非确定性高阶递归计划（HORS）：给定一个非确定性的HORS，决定这HORS生成的所有有限树的集合是否是有限的。我们给出一个类型系统，使得HORS可以生成任意大的有限大小的树当且仅当在类型系统中，我们可以获得任意大的导子，在适当的意义上，后一个条件可以很容易地决定。
2017-01-19 cs.FL cs.LO
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
