Fair Termination of Asynchronous Binary Sessions
本文提出基于线性逻辑的异步会话类型理论，利用新颖的公平异步子类型关系保证良类型进程在公平性假设下公平终止，实现无饥饿与无孤儿消息。
2025-03-14 cs.DC cs.LO cs.PL
A Logical Account of Subtyping for Session Types
本文在带不动点的线性逻辑框架下研究会话类型的子类型关系，提出一种同时保持安全性与终止性的子类型刻画，并证明该子类型在理论上可通过强制语义编译消除。
2023-04-13 cs.DC cs.LO cs.PL
Characteristic Formulae for Session Types (extended version)
子类型是会话类型论及其应用的关键组成部分，特别是在程序设计语言实现中。在本文中，我们研究了有效的方法来检查是否一个会话类型是另一个的子类型，通过应用特征公式的方法来解决这个问题。我们的核心贡献是一个算法来生成一个模态μ演算公式，该公式描述了给定类型的所有超类型（或子类型）。然后，子类型检查可以卸载到模型检查器，从而附带地产生一个有效的算法来检查会话类型的安全性，可靠而完整。我们已经实现了我们的理论，并比较其成本与其他经典的子类型算法。
2015-10-23 cs.LO
Relating Church-Style and Curry-Style Subtyping
具有高阶子类型或单例类型的类型论是变量的计算规则受上下文中的类型信息影响的系统的示例。这些系统的一个复杂之处是，在上下文中声明的边界不能很好地与完整性或终止性的逻辑关系证明交互。本文对F-Omega-Sub的类型语法提出了一种自然的修改，将变量的绑定添加到变量类型构造函数中，从而将变量的计算行为与上下文分离。F-Omega-Sub中的子类型算法可以在没有上下文或种类信息的类型上给出。因此，元理论遵循了上下文中没有计算信息的类型系统的一般方法，包括一个简单的逻辑关系定义，而没有上下文的Kripke风格索引。这种新的表示系统被证明是等价于传统的表示没有界限的变量类型构造函数。
2011-01-24 cs.LO cs.PL
Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)
针对单一组合子演算的终止性问题，改进基于SAT求解器的树自动机构造方法，成功证否了8个此前悬而未决的非擦除组合子的终止性。
2024-06-20 cs.FL cs.LO
Compositional Interface Refinement Through Subtyping in Probabilistic Session Types
本文提出概率混合选择多方会话π演算及其灵活子类型系统，允许用多个通道细化单个接口，并证明主体归约、无错误性和无死锁性，从而支持概率分布式通信的组合式验证与逐步细化。
2025-09-12 cs.LO
An Interactive Proof of Termination for a Concurrent $λ$-calculus with References and Explicit Substitutions
在本文中，我们介绍了一个类型化的，并发的$λ$ -演算的引用具有显式替换变量和引用。除了通常的安全属性，我们恢复了强正常化。证明是基于一个reductiontechnique和一个原始的互动属性让人想起游戏语义的方法。
2021-02-09 cs.LO cs.PL
A Calculus for Modular Loop Acceleration and Non-Termination Proofs
循环加速可以用来证明程序的安全性、可达性、运行时界限和（非）终止性。为此，已经提出了各种加速技术。然而，到目前为止，所有这些都是单一的，即，不能使用几种不同加速技术的组合来加速单个循环。相比之下，我们提出了一个演算，允许以模块化的方式结合加速技术，我们展示了如何将许多现有的加速技术集成到我们的演算。此外，我们提出了两种新的加速技术，可以无缝地纳入我们的微积分。其中一些加速技术仅适用于非终止循环。因此，将它们与我们的新演算相结合，产生了一种新的模块化方法来证明非终止性。实证评估表明，我们的方法的适用性，无论是循环加速和证明不终止。
2022-06-08 cs.LO cs.PL
A Theory of Higher-Order Subtyping with Type Intervals (Extended Version)
依赖对象类型（DOT）的演算使Scala的实现更加原则和健壮，但它对类型级计算的支持已被证明是不够的。作为补救措施，我们提出了$F^ω_{..}$，这是Scala的高级类型的严格理论基础。$F^ω_{..}$用区间类扩展了$F^ω_{<:}$，它提供了对Scala中重要的类型级和类级抽象机制的统一处理，例如有界量化、有界运算符抽象、半透明类型定义和第一类子类型约束。其结果是一个灵活的和一般的理论高阶子类型。我们证明了$F^ω_{..}$的类型安全性和类安全性，以及类型的弱规范化和子类型的不可判定性。我们所有的证据是机械化的Agda使用一个完全的语法方法的基础上遗传替代。
2021-07-05 cs.LO cs.PL
Precise subtyping for synchronous multiparty sessions
子类型的概念在理论和应用领域都有重要的作用：在lambda和并发演算以及程序设计语言中。健全性和完整性，一起被称为子类型的精确性，可以从两个不同的角度来考虑：操作和指称。前一种精确性最近在类型安全方面得到了发展，即当一个更大类型的项被期望时，一个更小类型的项的安全替换。后者的精确性是基于一个类型的外延，这是一个数学对象，它根据语言中其他表达式的外延来描述该类型的含义。本文的结果是一个同步多方会话演算的子类型的操作和指称的精确性。本文的创新之处在于引入了特征全局类型来证明运算完备性。
2016-02-11 cs.LO cs.PL
An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $π$-Calculus
公平终止是程序的属性，这些程序可能“在原则上”偏离，但“在实践中”终止，即在关于非确定性选择的解决方案的适当公平假设下终止。我们研究了$μ$ MALL $^\infty$的一个保守扩展，$^\infty$是线性逻辑中具有最小和最大不动点的乘性加性片段的无穷证明系统，使得割消对应于公平终止。证明项是$π$ LIN的过程，它是线性$π$演算的一个变体，具有（共）递归类型，可以将二进制和（某些）多方会话编码到其中。因此，我们获得了一个行为类型系统的$π$ LIN（和间接会话演算通过其编码到$π$ LIN），确保公平终止：虽然良好的类型的进程可能会参与任意长的交互，他们是公平的保证，最终执行所有挂起的动作。
2022-07-08 cs.LO cs.PL
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。
2023-09-01 cs.LO math.LO
A Minimal OO Calculus for Modelling Biological Systems
在本文中，我们提出了一个最小的面向对象的核心演算建模的生物概念的类型，产生于生物本体的形式主义的基础上长期重写。该演算实现了封装、方法调用、子类型和一种简单的重写继承形式，并且适用于以最流行的术语重写形式主义设计的模型。以形式实现的类可以在几个模型中使用，如编程库。
2011-09-07 cs.CE cs.LO
Complete Call-by-Value Calculi of Control Operators II: Strong Termination
本文刻画了完全按值调用 lambda-mu 演算的强终止性，基于 CPS 语义和并-交集类型系统，证明了强可规范化性的充要条件。
2021-03-01 cs.LO cs.PL
Quantitative Types for the Functional Machine Calculus
本文为带可变存储、I/O 和概率选择效应的 FMC 设计非幂等交类型，分别刻画机器终止/脊规范化与强规范化，并度量或界约归约代价。
2025-05-15 cs.LO
Proving Non-Termination by Acceleration Driven Clause Learning (Short WST Version)
本研究将原本用于约束霍恩子句可满足性分析的加速驱动子句学习（ADCL）演算适配至转移系统非终止性证明场景，在工具LoAT中实现并与前沿方法开展对比评估。
2023-07-19 cs.LO
Proving Non-Termination by Acceleration Driven Clause Learning
本文将加速驱动子句学习（ADCL）适配到迁移系统，提出 ADCL-NT 变体用于证明程序非终止性，并在 LoAT 工具中实现和评估。
2023-07-07 cs.LO
Rewriting modulo in Deduction modulo
我们研究的终止重写模一组方程的代数构造演算，扩展的构造演算的功能和谓词定义的高阶重写规则。在以前的工作中，我们定义了一般的语法条件的基础上的概念，可计算的闭包，以确保终止的组合重写和β-减少。在这里，我们表明，这一结果是保留时，考虑重写模一组方程，如果这些方程产生的等价类是有限的，方程是线性的，并满足一般的语法条件，也基于可计算闭包的概念。这包括方程，如结合性和交换性，并提供了一个原始的处理终止模方程。
2006-10-11 cs.LO
A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
Université de Lorraine（洛林大学）；CNRS（法国国家科学研究中心）；Inria（法国国家信息与自动化研究所）；Universidad Nacional de Quilmes（基尔梅斯国立大学）；Universidad Argentina de la Empresa（阿根廷企业大学）；Universidad de la República（共和国大学）
Lambda-SX是一种支持多种测量基的量子λ演算，通过类型系统实现对测量的灵活控制和组合推理，展示了在量子编程语言中整合多种基的可行性。
2025-08-21 cs.LO quant-ph
Session Types as Generic Process Types
行为型系统比通常的静态分析更安全。它们基于“类型即进程”的思想，为特定的属性提供专用的类型代数，从协议兼容性到竞争自由、锁自由甚至响应性。有两种成功的方法，尽管它们有很大的不同，它们是会话类型和进程类型。前者允许使用特定类型（证明）系统来指定和验证（分布式）通信协议;后者允许从系统规范中推断出一个过程抽象，使用通用类型（证明）系统可以更简单地验证属性。这些方法之间的关系是什么？一般的一个可以substantially具体的一个？代价是什么？前者可以作为后者的编译器吗？本文介绍的工作是朝着回答这些问题迈出的一步。具体地说，我们定义了一个逐步编码的pi演算会话和会话类型（系统的盖伊和孔）到一个pi演算的进程类型（通用类型系统的五十岚和小林）。我们对会话类型环境、极性（区分会话通道端点）和标记总和进行编码。我们展示了编码的正向和反向操作对应，以及类型对应。为了在进程类型子类型中忠实地编码会话子类型，需要向目标语言添加记录构造函数和新的子类型规则。总之，作为协议抽象的会话类型的编程便利性可以与pi演算的简单性和功能相结合，特别是利用通用类型系统提供的框架。
2014-08-07 cs.LO cs.PL
On the relation between size-based termination and semantic labelling
我们调查两个独立开发的终止技术之间的关系。一方面，基于大小类型的终止（sized-typesbasedtermination，SBT）使用带有大小表达式和Girard的reductioncandidates注释的类型，并且仅适用于使用构造函数匹配的系统。另一方面，语义标记通过用其参数的语义注释每个函数符号来转换重写系统，并且适用于任何重写系统。首先，我们介绍了一个简化版本的SBT的简单类型的Alzuda演算。然后，我们给出了新的证明的正确性SBT使用语义标签，在第一和高阶的情况下。因此，我们表明，SBT可以扩展到使用定义的符号（例如，关联函数）匹配的系统。
2009-06-23 cs.LO
Type theory and rewriting
我们研究的属性，特别是终止，依赖类型系统的λ演算和重写。
2007-02-22 cs.LO
A type-based termination criterion for dependently-typed higher-order rewrite systems
一些作者设计了基于类型的终止标准ML类语言允许非结构递归调用。我们将这些工作扩展到一般的重写和依赖类型，从而为构造演算中的重写和β-还原的组合提供了一个强大的终止标准。
2006-10-11 cs.LO cs.PL
Termination in Concurrency, Revisited
本文从终止性视角比较了 $π$-演算进程的两种类型系统（基于权重的方法与线性逻辑的 Curry-Howard 对应），揭示了它们之间的精确联系及其支持的客户端/服务器交互类别。
2023-08-02 cs.LO
On the Fair Termination of Client-Server Sessions
客户-服务器的【形】会话基于线性逻辑命题作为会话类型的传统解释的变体，其中非线性通道（调节客户端池和单个服务器之间的交互的通道）由共指数而不是通常的指数来类型化。共指数能够对竞争交互进行建模，从而客户端竞争与单个服务器进行交互，该服务器的内部状态（以及所提供的服务）可能会随着服务器顺序处理请求而发生变化。在这项工作中，我们提出了一个公平的终止结果CSLL $^\infty$，客户-服务器的【形】会话的核心演算。我们设计了一个类型系统，使得每个类型良好的术语对应于$μ$ MALL $^\infty$中的一个有效推导，$^\infty$是线性逻辑的最小和最大不动点的无穷证明理论。然后，我们建立了一个对应关系之间的减少在微积分和主要减少在$μ$ MALL $^\infty$。CSLL $^\infty$中的公平终止来自$μ$ MALL $^\infty$中的切割消除。
2022-12-11 cs.LO cs.PL
Embedding Pure Type Systems in the lambda-Pi-calculus modulo
本文证明通过添加计算规则扩展的 lambda-Pi-calculus modulo 具有惊人表达能力，可将系统 F 等函数式 Pure Type Systems 保守嵌入其中。
2023-10-19 cs.LO
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
在连续随机抽样和显式递归的λ演算中，基于排序上鞅，给出了几乎必然终止的一种证明方法。这一结果在三个方面得到了推广。反音排名函数对它们必须下降的速度限制较弱，并且适用于更广泛的程序。稀疏排名函数只在程序可达状态的子集上取值，因此定义起来更简单，也更灵活。排名功能方面的替代减少战略提供了更大的灵活性，并显着增加了适用性的排名上鞅的方法来证明几乎肯定的终止，由于一个新的（限制）合流的结果，这是独立的利益。反调排序函数的概念受到McIver、Morgan、Kaminski和Katoen在一阶命令式语言中的类似工作的启发，但适用于高阶函数式语言。稀疏排名功能和合流语义扩展是唯一的高阶设置。我们的方法可以用来证明几乎肯定终止的程序，是超出了文献中的方法，包括高阶和非仿射递归。
2021-04-30 cs.LO cs.PL
Mixed Choice Multiparty Session Types, Precisely
University of Oxford（牛津大学）
本文针对含会话委托等特性的混合选择多方会话类型，证明其子类型关系的精确性，开发通用类型系统并实现相关检查算法，经案例研究验证其有效性。
2026-08-12 cs.LO cs.PL
Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers
提出一种基于语义标注翻译和Blanqui一般模式的模块化终止性证明方法，实现为工具SOL，并成功应用于证明带代数效应处理器的调用-按-值演算变体的终止性。
2022-06-13 cs.LO cs.SC
A Superposition Calculus for Abductive Reasoning
Univ. Grenoble Alpes（格勒诺布尔阿尔卑斯大学）；CNRS（法国国家科学研究中心）；LIG（格勒诺布尔信息学实验室）
我们提出了一个修改的叠加演算是为了产生的一阶公理集的后果。这种方法被证明是健全的和演绎完整的冗余消除规则的存在下，所考虑的后果是建立在一个给定的有限的地面条款，由常数符号表示。与其他方法相比，大多数关于叠加演算终止的现有结果可以结转到我们的程序中。这特别确保了对于SMT社区感兴趣的许多理论来说，微积分是终止的。
2014-07-13 cs.AI cs.LO
Intersection Types and (Positive) Almost-Sure Termination
随机化高阶计算可以被看作是被赋予了单个代数运算的λ演算捕获的，即二元概率选择的构造。这种计算的重要性在于获得任何给定结果的概率，而不是获得它的可能性或必要性，就像在（非）确定性计算中一样。终止，可以说是最简单的可达性问题，至少可以用两种方式来解释，这取决于它是谈论收敛的概率还是期望的评估时间，第二个提供了更强的保证。在本文中，我们证明了交集类型能够精确地描述单个类型系统内的两个终止概念：任何λ项的收敛概率都可能被其类型低估，而底层推导的权重给出了项的期望值的下限。步骤到范式。值得注意的是，这两个近似都是紧的--不仅是可靠性，而且是完整性。关键的成分是非幂等性，没有它就不可能推理出完全评估任何项所需的约简步骤的预期数量。此外，我们还从理论上证明了所得到的近似是最优递归：没有递归可逼近的形式系统能比它做得更好。
2020-12-23 cs.LO
A dependently-typed calculus of event telicity and culminativity
Department of Mathematical Sciences, Carnegie Mellon University（卡内基梅隆大学数学科学系）；Department of Computer Science, Indiana University（印第安纳大学计算机科学系）
本文提出一种具有依赖类型的跨语言框架，用于分析事件的终态与终极性，结合实例展示如何用该框架建模英语句子。框架分为名词域和动词域，分别处理名词短语的界限性及其与子类型、限定量词和形容词修饰的关系，以及定义依赖事件演算，区分终态事件和终极事件，并考虑副词修饰。
2026-02-19 cs.CL cs.LO
Gödel Logic: from Natural Deduction to Parallel Computation
命题哥德尔逻辑用线性$A\rightarrow B\ \lor\ B\rightarrow A$的非构造性原理扩展了直觉主义逻辑。我们介绍了一个Curry-Howard对应这种逻辑，并表明，一个特别简单的自然演绎演算可以用作一个类型系统。由此产生的函数式语言丰富了简单类型的λ演算与并行进程之间的同步通信机制。我们的规范化证明采用了原始的终止参数和复杂的证明转换与有意义的计算阅读。我们的结果提供了一个计算解释哥德尔逻辑作为一个逻辑的通信并行进程，从而证明了Avron的1991年猜想。
2017-06-18 cs.LO
Cut elimination for the alternation-free modal mu-calculus
University of Gothenburg（哥德堡大学）；University of Amsterdam（阿姆斯特丹大学）
本文为模态μ-演算的无交替片段提出一种基于循环证明系统的语法切消去过程，利用多切和良拟序理论直接将带切证明转换为无切证明并保证终止。
2026-10-23 cs.LO math.LO
Type-Based Termination for Futures
本文将顺序语言中的大小类型终止性检查方法适配到并发场景，通过扩展半公理化相继式演算提出大小类型细化方案，借助无限宽有限深的类型推导树和新颖逻辑关系论证，实现基于futures的函数式并发程序的终止性验证。
2024-04-15 cs.LO cs.PL
A Step-indexed Semantics of Imperative Objects
步索引类型的语义解释被提出作为一种替代纯粹的句法证明类型安全使用主题约简。这些类型被解释为由计算步骤数索引的值集合，这些值被保证表现得像该类型的适当元素。艾哈迈德，阿佩尔和其他人的工作的基础上，我们引入了一个步骤索引的语义的命令对象演算的阿巴迪和Cardelli。由于动态分配对象、高阶存储和富有表现力的类型系统的结合，使用更“传统”的域理论方法来提供这种演算的语义帐户已被证明具有挑战性。在这里，我们表明，使用步进索引，可以解释一个丰富的类型纪律与对象类型，子类型，递归和有界量化类型的存在状态。
2009-12-18 cs.LO cs.PL
Semi-continuous Sized Types and Termination
一些基于类型的终止方法使用大小类型：数据结构大小的序数界限存储在其类型中。如果在类型系统中可见递归调用仅在较小的大小上发生，则接受大小调整类型上的递归函数。这种方法只有在递归函数的类型是可接受的情况下才是合理的，即，在某种程度上取决于大小指数。为了探索空间的容许函数在存在较高的kinded数据类型和impredicative多态性，语义的大小类型被解释为从序数到强规范化的条款集的功能。结果表明，上半连续的这种功能是一个充分的语义准则的可容许性。为了提供一个语法标准，半连续函数的演算。
2008-04-10 cs.LO cs.PL
Hypertableau Reasoning for Description Logics
University of Oxford（牛津大学）
我们提出了一种新的推理演算的描述逻辑SHOIQ^+-一个知识表示形式主义与应用领域，如语义Web。不必要的非确定性和大型模型的建设是两个主要来源的低效率的基于表的推理演算中使用的国家的最先进的推理机。为了减少不确定性，我们基于超表和超分辨率演算，我们扩展了阻塞条件，以确保终止。为了减少所构造模型的大小，我们引入了任意位置成对分块。我们还提出了一个改进的名义介绍规则，确保终止在存在的名义，逆角色，和数量限制-DL结构的组合，已被证明是出了名的难以处理。我们的实现显示出显着的性能改进，在国家的最先进的推理几个著名的本体。
2014-01-15 cs.AI cs.LO
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
我们提出了一个具有全局模态、自反性、传递性和角色层次的分级混合逻辑的终止表演算。系统的终止是通过基于模式的阻塞实现的。以前的相关逻辑方法都依赖于基于链的阻塞。除了在概念上简单，适合高效的实现，基于模式的方法给我们一个NExpTime的决策过程的复杂性。
2011-03-22 cs.LO
SCL(FOL) Revisited
本文精炼了一阶逻辑（无等式）的SCL演算，引入改编自SCL(T)的正则性概念以保证非冗余子句学习，并通过轨迹和模型界限实现终止，同时给出严谨的可靠性、完备性证明。
2024-03-19 cs.LO cs.SC
Curry and Howard Meet Borel
我们表明，计数命题逻辑的直观版本对应，在咖喱和霍华德的意义上，一个表达型系统的概率性事件的aldida演算，车辆演算，其中调用的名称和调用的离散随机函数程序的值评估可以模拟。值得注意的是，证明（分别是类型）不仅保证有效性（分别是终止性）成立，而且还揭示了潜在的概率。最后，我们表明，通过赋予类型系统的交集算子，得到一个系统，精确地捕捉概率行为的pendoda条款。
2022-03-21 cs.LO math.LO
A Generic Type System for Higher-Order $Ψ$-calculi
高阶$Ψ$演算框架（HO $Ψ$）是$π$演算的许多一阶和高阶扩展的推广。Parrow等人提出，高阶结石如HO $π$和CHOCS可以表示为HO $Ψ$ -结石。本文给出了HO $Ψ$ -演算的一个泛型类型系统，它扩展了Hüttel关于一阶$Ψ$ -演算的泛型类型系统的工作.我们的通用类型系统满足通常的属性的主题减少，并可以实例化产生类型系统的变体HOπ，包括类型系统的终止由于Demangeon等人。此外，我们推导出一个类型系统的$ρ$演算，反射高阶演算提出的Meredith和Radestock。这表明我们的泛型类型系统比它的前身更丰富，因为$ρ$ -演算不能以满足可编码性标准的方式编码在$π$ -演算中。
2022-09-06 cs.LO cs.PL
Type-theoretical natural language semantics: on the system F for meaning assembly
IRIT（图卢兹计算机研究所）；UPS（图卢兹第三大学）；LaBRI（波尔多计算机研究实验室）；Université de Bordeaux（波尔多大学）
本文提出并扩展了我们的类型理论框架的组成治疗的自然语言语义与一些词汇功能，如touchons（例如，一个城镇到一个足球俱乐部）和copredication（例如，在一个城镇作为一组人和作为一个位置）。二阶类型λ演算被证明是一个很好的框架，在这里我们讨论如何引入预定义类型和强制子类型，这比内部编码的类似结构更自然。这些新特征的语言应用也举例说明。
2013-03-12 cs.CL cs.LO math.LO
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
本文提出了一个wp风格的演算获得的概率程序的期望运行时间的界限。它的应用包括确定（可能无限）的期望终止时间的概率程序和证明积极的几乎必然终止-一个程序终止概率1在有限的期望时间？我们提供了几个证明规则的运行时间的循环，并证明了一个简单的操作模型的方法的可靠性。我们表明，我们的方法是一个保守的扩展Nielson的方法推理确定性程序的运行时。我们分析了一些示例程序的预期运行时间，包括一维随机游走和优惠券收集器问题。
2017-11-28 cs.LO cs.PL
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
自从Val Tannen的先驱工作简单类型的类演算和一阶重写的组合（LICS'88），许多作者都通过将其扩展到更丰富的类型类演算和重写范式，最终在演算像代数结构的演算。这些工作提供了理论基础的类型理论的证明助手的功能和谓词定义的定向高阶方程。这种定义包含了基于归纳的定义，更容易编写，并提供了更多的自动化。另一方面，检查用户定义的重写规则是强规范化和融合的，并且在与beta约简结合时保持类型检查的可判定性，则更加困难。大多数终止标准依赖于期限结构。在以前的工作中，我们扩展到依赖类型和高阶重写，“大小类型”的概念由几位作者在ML类语言的简单框架中研究，并证明了它保持了强规范化。本文件的主要贡献是双重的。首先，证明了在带尺寸标注的代数构造演算中，只要尺寸标注所产生的约束集是可满足的，并且允许最一般的解，则类型推断和类型检验问题是可判定的.其次，我们证明了一个大小代数足够丰富的捕获通常的归纳为基础的定义和更多的后来的属性。
2006-09-11 cs.LO cs.PL
Types by Need (Extended Version)
交叉演算理论的一个基石是交叉类型具有终止性。它们是一种灵活的工具，可以适用于各种终止概念，也可以产生适当的指称模式。自从de Carvalho在2007年的开创性工作以来，人们知道多类型（即非幂等交集类型）用定量信息和与线性逻辑的强联系来细化交集类型。通常，类型派生提供计算长度的界限，而最小类型派生提供精确的界限。De Carvalho研究了按名呼叫评估，Kesner使用他的系统来证明按需呼叫和按名呼叫的终止等价性。然而，De Carvalho的系统无法提供按需调用评估长度的精确界限。本文提出了一种新型的多类型按需呼叫系统。我们的系统产生精确的界限，并诱导一个指称模型的呼叫的需要，提供第一个严格的定量语义呼叫的需要。
2019-02-15 cs.LO cs.PL math.LO
When Types Intersect and Effects Get Handled
University Sorbonne Paris Nord（索邦巴黎北大学）；University of Bologna（博洛尼亚大学）；National Institute of Informatics（国立情报学研究所）
本文为带代数效果和处理器的λ-演算引入了一种新的交集类型系统，该系统具有行为性质，满足主题归约和扩展，能刻画终止项并可将可达性问题归约到类型推断，同时诱导出一个简单类型系统，其类型可靠且HOMC问题可判定。
2026-08-26 cs.LO cs.PL
Extending the Quantitative Pattern-Matching Paradigm
本研究扩展非幂等交集类型系统以刻画带模式匹配的函数式编程语言的终止性，并证明其定量性质，即类型推导大小可上界求值步数。
2024-08-20 cs.LO cs.PL
Transformer Models for Type Inference in the Simply Typed Lambda Calculus: A Case Study in Deep Learning for Code
IHES（高等科学研究所）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；IBM Research（IBM研究院）
本文提出以项与类型关系为核心的基准，研究 transformer 在简单类型 lambda 演算类型推断中的预热与优化器选择，发现 Adafactor 较 Adam 和 RAdam 收敛更快。
2023-03-15 cs.AI cs.LG cs.LO
Types of Fireballs (Extended Version)
Plotkin的按值调用演算的良好性质主要依赖于对弱求值和闭项的限制。开放式按值调用是更一般的设置，其中评估较弱，但条款可能是开放的。这种延伸是微妙的，文献中载有一些建议。最近，Accattoli和Guerrieri对这些建议进行了详细的业务和实施研究，表明从终止的角度来看，它们是等同的，而且在时间成本模型一级也是如此。本文探讨了开放的按值调用的指称语义，通过多类型（又名非幂等交集类型）改编de Carvalho的按名称调用的分析。我们的类型系统的特点规范化，从而提供了一个足够的关系语义。此外，类型推导进行定量信息的成本评估：其大小的边界的数量的评估步骤和大小的范式，我们也推导出精确的界限。这项研究主要依赖于一个新的，完善的介绍火球演算，最简单的建议，开放调用的价值，这是更容易的外延调查。
2018-10-29 cs.LO math.LO
A type theoretical framework for natural language semantics: the Montagovian generative lexicon
LaBRI, Université de Bordeaux（波尔多大学LaBRI实验室）；IRIT-CNRS, Toulouse（图卢兹信息学研究所-法国国家科学研究中心）
我们提出了一个框架，命名为蒙塔哥维生成词典，用于计算自然语言句子的语义，表示在许多排序的高阶逻辑。词义由二阶λ演算（Girard系统F）的λ项描述，其基本类型包括用于命题的类型和用于多排序逻辑的排序的多类型。这个框架能够将对词汇现象的适当处理整合到蒙塔格维的组合语义学中，包括对谓词的论元性质施加的选择限制，以及词义对某些上下文的可能适应。在这些适应一个词的意义的上下文中，本体论的包容性处理的强制子类型，在本文中介绍的系统F的扩展。这一框架的词汇语用学的好处是说明意义转移和转换，在不同的意义上的可能和不可能的copredication，对deverbal歧义，和“虚构的运动”。接下来，我们表明，组成治疗的限定词，量词，复数，…在我们的框架中是细粒度的。最后，我们从语言学、逻辑学和计算学的角度对蒙塔哥夫生成词典进行了总结。
2014-01-03 cs.CL cs.LO
Dependent Type Refinements for Futures
本文提出将依值类型细化应用于基于 future 的进程演算 SAX，综合无穷证明论、双向类型检查与 Hoare logic，实现了支持 codata 信息隐藏的程序部分正确性推理，并证明了语法类型可靠性。
2023-11-18 cs.LO cs.PL
