Full Abstraction for a Recursively Typed Lambda Calculus with Parallel Conditional
我们定义了一个递归类型的λ演算的语法和约简关系，并给出了一个并行的条件函数。减少显示为融合性。我们将递归类型解释为受限形式的信息系统，我们称之为素系统。一个指称语义定义与此解释。定义了项的语法范式逼近，证明了逼近定理：项的语义等于其逼近的语义的极限。证明使用包含谓词（逻辑关系）。对于布尔值的观察，语义是足够的。在平行格功能的存在下，它也是完全抽象的。
2008-06-11 cs.LO
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence
本文证明在函数元数和变量数有界时，渐近几乎每个阶为k的简单类型化λ项都有长度达(k-1)重指数的β-归约序列，通过推广无限猴子定理实现，服务于高阶模型检测的定量分析。
2019-02-21 cs.LO
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search
依赖类型的lambda演算，如逻辑框架（LF），能够通过类型表示术语之间的关系。通过利用“公式作为类型”的概念，这种演算也可以在类型判断中编码公式及其证明之间的对应关系。因此，这些演算提供了一个自然而强大的手段来指定各种形式系统。这样的规范可以被转换成更直接的形式，该形式在简单键入的非线性项上使用谓词公式，从而使用传统的逻辑编程技术为它们的动画提供基础。然而，这种想法的天真使用充满了效率低下的事实，依赖类型的表达式通常包含大量冗余的类型信息。我们研究的句法标准识别，因此，消除这种冗余。特别是，我们确定了LF类型中的绑定变量的属性，称为“刚性”，并正式表明，检查这些变量的实例化遵守类型限制是不必要的，以确保整体表达是良好的。我们将展示如何利用这一属性在一个基于翻译的方法来执行规范的BMPF语言。识别冗余也与设计依赖类型表达式的紧凑表示有关。我们强调我们工作的这一方面，并讨论它与在这方面提出的其他方法的联系。
2010-07-05 cs.LO
Strong Typed Böhm Theorem and Functional Completeness on the Linear Lambda Calculus
本文证明了线性λ演算上的类型化Böhm定理的一个版本，即对于任意给定的类型A和B，当给定A的两个不同的闭项s1和s2以及B的任意闭项u1和u2时，存在一个项t使得ts1可转换为u1，ts2可转换为u2.几年前，这个定理的一个较弱的版本被证明，但更强的版本是开放的。作为这个定理的推论，我们证明了：如果A有两个不同的闭项s1和s2，则A关于s1和s2是函数完备的。到目前为止，只知道有几种类型的功能是完整的。
2016-04-05 cs.LO
Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi
在本文中，我们使用有限向量空间（有限维，在有限域上）作为线性逻辑的非标准计算模型。我们首先定义了一个简单的，有限的PCF类布尔演算，然后我们讨论了两个有限的模型，一个基于有限集，另一个基于有限向量空间。第一个模型被证明是完全完整的操作语义的语言。第二个模型是不完整的，但我们开发了一个代数扩展的有限λ演算，恢复完整性。描述了这两种语义之间的关系，并给出了几个基于Church数词的例子。
2014-06-05 cs.LO
Definable functions in the simply typed lambda-calculus
简单型λ演算中可定义的整数函数都是扩张多项式，这是一个常识。当我们在类型（p->p）->p->p上解释整数时确实是这种情况，其中p是基本类型和/或相等被视为beta转换。通常认为，这同样适用于beta-eta等式和表示在任何固定类型的形式（t->t）->t->t上的整数。在本文中，我们表明，这种意见是不完全正确的。本文证明了在简单型λ演算中严格可定义的函数类比广义多项式大得多。也就是说，我们定义F为严格可定义函数的类，G为包含扩展多项式和两个附加函数的类，或者更准确地说，两个函数模式，并且在复合下是封闭的。我们证明了G是F的一个子集。我们猜想G精确地刻画了严格可定义的函数，即G=F，并且我们为这个猜想收集了一些证据，例如，证明了每个可斜表示的有限值域函数在（t->t）->t->t上对某些t是严格可表示的。
2007-01-04 cs.LO
On Encoding LF in a Predicate Logic over Simply-Typed Lambda Terms
Festival和Miller描述了他们声称是遗传Harrop公式逻辑中依赖类型化的λ演算LF的忠实编码，这是Church简单类型论的直觉变体的子逻辑。它们的编码大致基于将LF中的对象表达式转换为简单类型的λ演算中的项，方法是在类型化中擦除依赖关系，然后通过使用谓词重新捕获擦除的依赖关系。不幸的是，这个想法并不完全奏效。特别是，我们提供了一个反例，声称所描述的编码是忠实的。这种说法错误的根本原因是，从依赖类型的lambda项到简单类型的lambda项的映射不是一对一的，因此逆变换是模糊的。这一观察对其他相关编码有广泛的影响。
2021-08-24 cs.LO cs.PL
Two Decreasing Measures for Simply Typed Lambda-Terms (Extended Version)
本文针对简单类型λ演算提出W-测度与Tm-测度两种构造性递减测度，借助非擦除的m-演算辅助系统，基于归约式度数不升高的性质，分别用自然数和嵌套多重集刻画，为强规范化提供了新的构造性证明途径。
2023-04-29 cs.LO
A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms
与其他几个lambda项家族相反，没有封闭公式或生成函数是已知的，并且在分析组合学中设计的复杂技术目前都不能帮助计数或生成给定大小的{ \em简单类型封闭lambda项}的集合。此外，它们在闭lambda项集合中的渐近稀缺性使得通过蛮力生成和类型推断来计数它们变得非常困难，以前发表的工作显示它们的计数仅达到10。通过利用逻辑变量之间的协同作用，统一与发生检查和有效的回溯，在今天的Prolog系统，我们爬4个数量级以上的先前已知的计数，通过推导出越来越快的霍恩子句程序，生成和/或计数的一组封闭的简单类型的lambda项的大小高达14。对于{ \em闭简单类型范式}的类似计数也被导出到大小14。{ \em { \bf Keywords：}逻辑编程转换、类型推断、lambda项的组合学、简单类型λ演算、简单类型范式。}
2016-08-12 cs.LO cs.PL
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
一个新的，全面的方法来解决居住问题的简单类型的λ演算，处理决策和计数问题。这种方法的工作原理是利用一个表示的搜索空间所产生的一个给定的居住问题，这是在一个证明搜索，作者最近开发的微积分。这种表示可以被看作是通过类元项扩展证明的Curry-Howard表示，保持在λ演算和类型系统的方法内。我们的方法揭示了归纳描述的决策问题，由证明搜索表达式的语法驱动，最终产品是简单的，递归的决策程序和计数功能。
2017-03-11 cs.LO math.LO
Typed lambda-calculi and superclasses of regular functions
我们建议在类型化的布尔代数演算中使用Church编码作为隐式计算复杂性的自动机理论对应物的基础，就像一元二阶逻辑提供了描述复杂性的对应物一样。具体来说，我们研究转换，即串到串（或树到树）函数-特别是那些具有超线性增长的函数，如多正则函数，HDT 0 L转换和Sénizergues的“k-可计算映射”。我们对这一目标的第一个结果包括显示列入一些转导类在某些类定义的Alzoda-calculi。特别是，这揭示了一个基本的开放式问题的表现力的简单类型的Alzida演算。我们还编码正规函数（并通过改变考虑的程序类型，我们得到一个更大的子类的多正则函数）在基本仿射代数演算，一个变量的线性逻辑最初设计的隐式计算复杂性。
2019-06-30 cs.FL cs.LO
Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus
本文从范畴和代数的角度研究了类型化λ演算的赋值正规化问题。本文的第一部分通过Kripke逻辑关系分析了Jung和Tiuryn的lambda可定义性结果，并展示了它如何适用于统一可定义性和规范化，产生一个扩展的规范化结果。在第二部分的文件的分析进一步细化考虑内涵Kripke关系（在阿丁胶合的形式），并显示提供一个功能的规范化条款，铸造规范化的范畴胶合的背景下进行评估。技术发展包括类型化λ演算的语法和语义的代数处理，其允许在简单类型化元理论内给出规范化函数的定义。合成依赖类型的函数式程序设计语言中的求值规范化程序。
2022-08-18 cs.LO math.CT
Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form
依赖类型的lambda演算（英语：Lambda calculi），如Edinburgh逻辑框架（英语：Edinburgh Logical Framework）（LF），是一种流行的方式，用于编码关于正式语法对象的基于规则的规范。在这些框架中，通过使用类型的依赖结构，自然地捕获了表示形式对象的术语上的关系。我们在这里考虑在简单类型的λ-项上将以这种风格编写的规范保持意义地翻译成谓词逻辑。这样的翻译可以为高效的实现和推理规范的复杂能力提供基础。我们开始与先前描述的翻译LF规范的公式在逻辑的高阶遗传Harrop（hohh）公式。我们展示了如何通过识别和消除其中包含的冗余类型检查信息来改进这种翻译。这既有利于翻译公式的清晰度，又减少了执行过程中必须花费在类型检查上的精力。为了允许这种翻译被用来执行LF规范，我们描述了一个逆变换从hohh项LF表达式，因此可以使用翻译的形式进行计算，然后可以将结果导出回LF。基于LF规范的执行还可能涉及某些形式的类型重构。我们讨论的可能性，支持这样的能力，使用翻译的结构规范的一些合理的限制。
2013-10-31 cs.LO
On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
AIST Tsukuba Japan（产业技术综合研究所筑波日本）
本文证明任意多重值函数可通过第二阶多态类型系统的线性lambda项表示，采用两种不同风格，并讨论了优化方法及跨领域应用案例。
2026-03-27 cs.LO cs.PL
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
我们研究了一类简单类型的λ演算的名义代数Henkin式模型，其中变量映射到表示中的名称，而λ演算抽象映射到（非功能性的）名称抽象操作。由此产生的表示更小，更好的行为，在我们精确的方式，比基于函数值的模型。使用这些新的模型，我们然后开发了一个概括的λ-长期语法丰富他们的存在元变量，从而产生一个理论的不完整的功能。这种不完备性与函数抽象和应用给出的不完备性的通常概念是正交的，并且对应于洞和不完备对象。
2011-11-01 cs.LO cs.PL
A Typed Lambda-Calculus for Establishing Trust in Probabilistic Programs
针对概率程序无法用传统正确性衡量的问题，提出一种类型化λ演算框架，通过运行时实验算子和静态置信度概念，形式化输出频率与预期分布一致的信任概念，证明其符合概率论原理。
2025-02-14 cs.LO
Weak Typed Boehm Theorem on IMLL
在克里特岛的Boehm定理研讨会上，Zoran Petric称Statman的“典型模糊性定理”为Boehm定理。此外，他还基于简单类型的λ演算的集合理论模型给出了该定理的新证明。在本文中，我们研究的线性版本的类型Boehm定理的直觉线性逻辑的一个片段。证明了在不含乘法单位1的直觉线性逻辑的乘法片段（简称IMLL）中弱型Boehm定理成立。IMLL系统完全对应于线性λ演算没有指数，添加剂和逻辑常数。IMLL系统也恰好对应于没有单位对象的自由对称monoidal闭范畴。据我们所知，我们的分离结果是第一个关于这些系统在一个纯粹的语法方式。
2005-04-16 cs.LO
The Formal System lambda-delta
形式化系统lambda-delta是一种类型化的λ演算，它以术语、类型、环境和上下文的统一为主要目标。lambda-delta从Automath相关的lambda演算和纯类型系统中获得了一些功能，但与两者不同的是，它不包括Pi结构，而在术语级别提供了缩写机制。Delta-delta具有一些重要的理想性质，如归约的汇合性、类型的正确性、转换前类型的唯一性、类型赋值的主体归约性、类型化项的强规范性以及作为推论的类型推断问题的可判定性。
2008-09-25 cs.LO
One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus
该研究针对简单类型λ演算的反合一问题，突破现有研究仅关注禁止泛化变量嵌套的幺正变体的局限，证明含嵌套泛化变量时该问题为零元，为泛化方法的扩展应用提供理论支撑。
2024-03-15 cs.LO
A concrete model for a typed linear algebraic lambda calculus
本文为带测量的类型化线性代数 lambda 演算 Lambda-S 构造了基于集合与复向量空间范畴伴随关系的具体模型，用隐藏的遗忘函子解释叠加类型 S。
2023-10-11 cs.LO math.LO
Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations
本文为Wansing双直觉主义逻辑2Int构建双类类型化λ演算λ-2Int，建立带项标注的证明系统并证明对偶化定理，从而从双边主义视角探讨证明的意义、指称与同一性问题。
2024-02-23 cs.LO math.LO
A call-by-value lambda-calculus with lists and control
微积分与控制运营商已被研究的原因控制程序设计语言和解释经典证明的计算内容。为了使这些演算成为真正的程序设计语言，还应该包括数据类型。作为向这个方向迈出的一步，本文定义了一个简单类型的按值调用λ演算，它具有控制操作符catch和throw、列表的数据类型和用于原语递归的操作符（类似于Goedel的T）。我们证明了我们的系统满足主题减少，进步，合流无类型的条款，以及良好的类型条款的强规范化。
2012-10-11 cs.LO
On Generalized Metric Spaces for the Simply Typed Lambda-Calculus (Extended Version)
广义度量，从Lawvere的度量空间丰富的范畴的观点，已被广泛应用于指称语义作为一种方式来衡量在何种程度上两个程序的行为相似，但不等价的方式。然而，到目前为止，将广义度量应用于高阶语言（如简单类型的λ演算）并不令人满意。本文研究了广义度量空间的Carnival闭范畴的一种新的构造方法。我们的出发点是一个定量语义学的基础上，一般的逻辑关系。在这种情况下，我们表明，几个家庭的广义度量提供的方法来扩展欧几里德度量的所有高阶类型。
2021-04-27 cs.LO cs.PL math.LO
Light types for polynomial time computation in lambda-calculus
本文提出了一种新的类型系统：对偶轻仿射逻辑（DLAL），它保证了类型良好的程序可以在多项式时间内执行。DLAL有一个简单的类型语言，带有线性和直观的类型箭头，以及一个模态。它对应于光仿射逻辑（LAL）的一个片段。我们表明，相反的LAL，DLAL确保良好的性能上的主题减少是满意的，一个良好的类型的长期承认多项式约束的减少任何策略。我们建立，作为LAL，DLAL允许代表所有的多时间功能。最后给出了命题DLAL的一个类型推断过程。
2004-05-11 cs.LO
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus
我们提出了一个形式化的会话类型在多线程λ演算（MTLC）配备了一个线性类型系统，建立MTLC类型保存和全球的进步。后者（全局进度）意味着在MTLC中对良好类型程序的评估永远不会陷入死锁。由于这个制定的MTLC可以很容易地嵌入到ATS，一个成熟的语言与功能的编程核心，支持依赖类型（的DML风格）和线性类型，我们得到了一个直接实现的会话类型在ATS。此外，我们获得了直接支持的依赖会话类型的基础上，这种嵌入到ATS的形式。与现有的各种会话类型的形式化相比，我们看到本文给出的形式化在其接近具体实现方面是独特的。特别是，我们报告这样一个实现准备实际使用，生成Erlang代码从良好类型的ATS源（利用会话类型），从而充分利用的基础设施支持分布式计算在Erlang。
2016-03-11 cs.LO cs.PL
Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
UCLA Department of Philosophy（加州大学洛杉矶分校哲学系）
本文提出结合模态逻辑与简单类型λ演算的参数化系统λ_θ，通过组合逻辑给出其模型刻画，并证明λ_θ与最大系统λ_ω之间的语义守恒与可表达性结果。
2026-07-14 cs.LO math.LO
Typed Answer Set Programming and Inverse Lambda Algorithms
Arizona State University（亚利桑那州立大学）
我们更广泛的目标是将英语句子自动翻译成适当的知识表示语言中的公式，作为理解和回答英语文本问题的一步。本文的重点是回答集编程语言（ASP）。我们的方法来翻译句子ASP规则的启发蒙塔古的使用λ演算公式的单词和短语的意义。以ASP为目标语言，单词和短语的含义是ASP-lambda公式。在早期的工作中，我们通过手动开发单词字典及其ASP lambda公式来说明我们的方法。然而，这种方法是不可扩展的。在本文中，我们的重点是两个算法，允许一个以逆的方式构建ASP-lambda公式。特别地，这两个算法将两个微积分表达式G和H作为输入，并且计算微积分表达式F，使得输入为G的F（由F@G表示）等于H;并且类似地G@F = H。我们目前的正确性和复杂性的结果，这些算法。为了做到这一点，我们开发了类型化ASP-λ演算理论及其顺序的概念，并将其用于开发完备性结果。(To《逻辑程序设计的理论与实践》（Theory and Practice of Logic Programming）
2012-10-21 cs.AI cs.LO cs.PL
On the Simply-Typed Functional Machine Calculus: Categorical Semantics and Strong Normalisation
本文研究函数机器演算（FMC）的范畴语义与强正规化，证明其在适当等式理论下对应自由笛卡尔闭范畴，并扩展 Gandy 证明以确立带类型 FMC 项的强正规化性质。
2023-05-25 cs.LO
Implicit automata in typed $λ$-calculi II: streaming transducers vs categorical semantics
本文将正则字符串转换刻画为带加法算子的线性 λ-演算程序，通过编码无复制流式字符串转换器并利用范畴语义学建立等价关系，进而将结果推广至树结构并揭示其与线性逻辑的联系。
2021-08-25 cs.FL cs.LO
A Theory of a Two-Dimensional Typed Lambda Calculus
Universidad Militar Nueva Granada (UMNG)（新格兰达军事大学）；Microsoft（微软）；Universidade Federal de Pernambuco (UFPE)（伯南布哥联邦大学）
提出一个二维类型化λ演算，以计算性路径作为相等性证据，通过递归证明性质，引入高阶相干律和路径类型，并用奇偶不变量证明系统一致且真正内涵，在Idris 2中完全形式化。
2026-09-18 cs.LO
Simply typed convertibility is TOWER-complete even for safe lambda-terms
本文证明 Blum–Ong 安全 λ-演算中的 β-及 βη-可转换性仍为 TOWER 完全，将此前 PSPACE 难的下界提升至塔层完全。
2024-09-04 cs.LO cs.PL
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
本文证明了有限PCF在加入异常、代数效应和引用等副作用后的四种扩展的不可判定性，并针对带引用的扩展提出了首个包含引用单元的高阶递归函数的非平凡可判定片段。
2025-02-10 cs.LO cs.PL
Verification of Ptime reducibility for system F terms via Dual Light Affine Logic
在以前的工作中，我们介绍了双轻仿射逻辑（DLAL）（[BaillotTerui04]）作为轻线性逻辑的一个变体，适用于保证复杂性的性质上的微积分条款：所有类型的条款可以评估在多项式时间和所有Ptime函数可以表示。在目前的工作中，我们解决的问题，在二阶DLAL的类型的DLDA项。为此，我们给出了一个过程，从系统F中的一个项开始，找到所有可能的方法将其装饰成DLAL类型的项。我们表明，我们的程序可以运行在时间多项式的大小，原来的教会类型的系统F项。
2006-03-27 cs.LO
Categories with Families: Unityped, Simply Typed, and Dependently Typed
我们展示了无类型的，简单类型的和依赖类型的λ演算的范畴逻辑如何可以围绕具有家族的范畴（cwf）的概念来构造。为此，我们引入简单类型的cwfs（scwfs）的子类别，其中类型不依赖于变量，和unityped cwfs（ucwfs），其中只有一个类型。我们证明了几个等价和双等价定理之间的cwf为基础的概念和基本概念的范畴逻辑，如carniveroperads，Lawvere理论，范畴有限的产品和限制，carniver-closed范畴，局部carniver-closed范畴。这些定理中的一些依赖于上下文（在Cartmell的意义上）或民主（由Clairambault和Dybjer用于他们的双等价定理）的限制。有些定理是严格保持所选结构的概念之间的等价。另一些是概念之间的双等价，其中属性只保留到同构。除此之外，我们还讨论了初始ucwfs，scwfs和具有额外结构的cwfs的各种构造。
2020-07-07 cs.LO
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Deepomatic；CNRS（法国国家科学研究中心）；Université Sorbonne Paris Nord（索邦巴黎北大学）；Université de Paris（巴黎大学）
反向传播是一种经典的自动微分算法，用于计算由某类简单的一阶程序（称为计算图）指定的函数的梯度。它是多个领域的基本工具，最值得注意的是机器学习，它是有效训练（深度）神经网络的关键。近年来，一个名为可微程序设计的研究领域迅速发展，其目的是通过求助于实际的程序设计语言，赋予控制流算子和高阶组合子，如map和fold，更综合和模块化地表达计算图。在本文中，我们将反向传播算法扩展到这样的一个程序设计语言的一个范例：我们定义了一个组合程序转换从简单类型的λ演算本身增加了一个概念的线性否定，并证明了这计算梯度的源程序具有相同的效率作为一阶反向传播。转换是完全无效果的，因此提供了对反向传播动态的纯逻辑理解。
2019-11-06 cs.LG 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
An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)
Turin University（都灵大学）；Toho University（东海大学）
提出一种带有零、后继和条件算子的无穷Lambda演算，通过全局迹条件确保良类型项的任何无穷归约都强收敛，并证明其与哥德尔系统T等价。
2026-06-24 cs.LO
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
在约简证明搜索中，证明自然地被解广义化，包括由局部正确的、自底向上的推理规则应用生成的所有可能的无限结构。我们提出了一个扩展的库里-霍华德范式的代表性，从证明到解决方案：代表解决方案可能是无限项的一个专用的微积分。这种新的，全面的方法证明搜索的例子与直觉蕴涵逻辑的演算LJT。提出了一种有限表示法，它包括用一个形式最大不动点扩展的类项，以及一个可以看作是共归纳证明逻辑的类型系统。在有穷系统中，定点变量享有宽松的绑定形式，允许通过类型系统检测循环。在搜索过程中，形式和用于表示备选项。此外，正式总和中使用的共归纳语法来定义“decontraction”（自下而上的收缩）-一个操作的理论，我们在本文中启动。作为一种语义，我们分配一个共归纳项到每个有限项。主要结果是存在一个等价的有限表示的任何完整的解决方案空间表示共归纳。这一结果是证明我们的共归纳证明逻辑在共归纳语义上是健全和完备的主要因素。这些结果是证明搜索的原始方法的基础，其中搜索建立了完整解空间的有限表示，并且后验分析通常包括应用语法指导的过程或函数。本文说明了这一点证明搜索和居住问题的简单类型的Alzada演算，审查结果详细其他地方，并包括新的结果，获得广泛的推广所谓的单原子定理。
2021-07-29 cs.LO math.LO
The Vectorial Lambda Calculus Revisited
我们重新讨论向量λ演算，它是线性的类型化版本。向量（以及线性）最初是为量子计算设计的，作为系统F的扩展，其中lambda项的线性组合也是项，类型的线性组合也是类型。在其第一个演示中，Vectorial只提供了Subject Reduction属性的弱化版本。我们证明了我们修改后的向量λ演算支持标准版本的属性，回答了一个长期存在的问题。此外，我们还引入了类型权和项权的概念，并证明了项权与其类型权之间的关系。
2021-05-14 cs.LO
A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
我们描述了一个类型系统的线性代数λ演算。类型系统解释了语言中模拟线性运算符和向量的部分，也就是说，它能够静态地描述程序归约所产生的项的线性组合。这就产生了一个原始的类型论，在这个理论中，类型可以像项一样叠加成线性组合。我们表明，所得到的类型的λ演算是强规范化和功能弱主题减少。
2012-07-31 cs.LO
Recovering Purity with Comonads and Capabilities
在本文中，我们采用了一种普遍有效的（ML风格的）类型λ演算，并展示了如何扩展它以允许捕获具有类型的纯表达式。我们的关键观察是，正如纯简单类型的λ演算可以扩展到支持一元类型规则的效果，不纯类型的λ演算可以扩展到支持一元类型规则的纯度。我们通过一个简单的指称模型来建立我们的类型系统的正确性，我们称之为能力空间模型。我们的模型形式化的直觉常见的系统程序员，执行效果的能力应该通过访问权限或能力进行控制，一个程序是能力安全的，如果它没有执行效果，它没有一个运行时的能力。然后，我们确定的公理范畴结构的能力空间模型验证，并使用这些公理给我们的comonadic类型系统的范畴语义。然后，我们给出了一个等式理论（替代和调用的值$β$和$η$法律）的命令λ演算，并显示其可靠性相对于此语义。最后，我们给出了一个翻译的纯简单类型的λ演算到我们的共同命令演算，并表明，任何两个条款是$βη$ -平等的STLC是平等的共同命令演算的方程理论，建立纯程序可以映射到我们的命令演算在一个方程保持的方式。
2020-11-10 cs.LO cs.PL
A theory independent Curry-De Bruijn-Howard correspondence
本文提出一种理论无关的通用参数化λ演算，将证明表达与具体理论选择解耦，从而统一实现柯里-德布鲁因-霍华德对应。
2023-04-17 cs.LO
Realizability in the Unitary Sphere
本文提出了一种基于可实现性的线性代数演算的语义。这种语义描述了系统中统一性的概念，回答了一个长期存在的问题。我们从语义中推导出一组简单类型的线性代数演算的类型规则，并展示了它如何扩展到经典和量子代数代数演算。
2019-04-18 cs.LO
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Curien和Herbelin的λ mu mu-演算的按名称调用版本的直观片段被隔离，并通过嵌入到简单类型的λ mu-演算中来证明其强规范化。我们的嵌入是一个延续和垃圾传递风格的翻译，灵感来自Ikeda和Nakazawa的Parigot的λ\_mu演算的翻译。嵌入严格模拟约简，而通常的连续传递式转换删除置换约简步骤。对于我们的直觉主义微积分，我们甚至只需要传递“垃圾单元”。我们将同样的方法应用于其他演算，即简单类型演算的连续扩展导致我们的直觉系统，并且已经对于我们考虑的最简单的扩展（具有广义应用的演算），这产生了通过约简保持嵌入的强规范化的第一个证明。所得到的结果扩展到第二和更高的阶结石。
2009-05-25 cs.LO
Clones, closed categories, and combinatory logic
本文用多元结构阐释简单类型λ演算的语义，引入外延SK-克隆并证明其可靠完备，进而证明不含产品的简单类型λ演算是SK-范畴的内部语言。
2024-05-02 cs.LO math.CT
A Categorical Normalization Proof for the Modal Lambda-Calculus
本文为模态λ-演算提出基于Kripke式替换的求值归一化算法，证明其可靠完备，为元编程的依赖类型基础奠定逻辑基石。
2023-02-20 cs.LO cs.PL
Linear Recursion
我们定义了两个扩展的类型的线性代数演算，产生最小的图灵完备系统。扩展是基于无界递归在一种情况下，和有界递归与最小化在其他。我们表明，这两种方法是兼容的线性和可键入性的限制。类型化线性代数演算的两个扩展都是最小的，在这个意义上，去掉任何组件都会破坏系统的普适性。我们讨论的实施技术，利用线性的结石。最后，我们将结果应用于语言的不动点算子：我们给出了一个编译的程序设计语言PCF成线性代数演算与线性无界递归。
2016-11-25 cs.LO cs.PL
A finiteness structure on resource terms
在我们的论文“Uniformity and the Taylor expansion of ordinary Aldada-terms”（与Laurent Regnier合作）中，我们研究了将Aldada-terms翻译为资源Aldada-terms的无限线性组合，这是基于微分线性逻辑和微分Aldada-演算的思想，从类似于Boudol的带资源Aldada-演算的演算开始的。这个翻译的好特性是。β归约由关于资源项的相干关系保证：归一化是“线性和稳定的”（在线性逻辑的相干空间语义的意义上）WRT。这种连贯性关系。当我们考虑非确定性的或代数的扩展时，这种相干性就丧失了（代数的非确定性的扩展是非确定性的扩展，其中的项可以线性组合）。我们引入了一个“有限性结构”的资源方面，导致一个线性拓扑向量空间结构的条款，并防止出现无穷大的系数在减少，在类型设置。
2010-01-19 cs.LO
Ticket Entailment is decidable
我们证明了票蕴涵的可判定性。Anderson和Belnap在关联逻辑的框架内提出的这个问题等价于具有部分基BB'IW的简单类型组合逻辑中的类型栖居的可判定性问题。本文解决了单纯型微积分对遗传右极大项的限制的类型栖居等价问题。
2012-07-05 cs.LO
How to generate random lambda terms?
我们调查了几种方法产生大的随机的双曲项，专注于他们的封闭和简单类型的变体。我们讨论了精确和近似大小生成的方法，以及实现大小均匀和非均匀结果分布的方法。
2020-05-19 cs.DS cs.LO cs.SE
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。
2016-09-05 cs.LO cs.PL
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
A revised completeness result for the simply typed $λμ$-calculus using realizability semantics
本文为简单类型lambda-mu-演算提出新的可实现性语义，证明可类型化项满足其类型解释，并利用特定项模型证明完备性，修正了先前文献中的错误。
2017-08-21 cs.LO math.LO
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
