Semantics of Typed Lambda-Calculus with Constructors
我们提出了一个Curry风格的二阶类型系统，具有并集和交集类型的Arbiser，Miquel和Rios的构造器的λ演算，扩展的λ演算与可变构造器的模式匹配机制。然后，我们证明了强规范化和匹配失败的限制，这个系统的情况下，通过适应标准的reductionmethod。
2011-03-16 cs.LO
Confluence Results for a Quantum Lambda Calculus with Measurements
证明了带测量的量子微积分Q* 的一个强收敛结果。更准确地说，合流举行有限和无限的计算。融合证明中使用的技术是语法上的，但具有创新性。这使得Q* 不同于类似的量子lambda演算，后者要么是无测量的，要么是提供了一个约简策略。
2009-05-28 cs.LO
Models and theories of lambda calculus
本文对Manzonetto博士论文中关于纯无类型代数演算的指称语义和等式/序理论的内容作了简要的总结。主要的研究成果包括：（1）从自反对象构造了一个一般的自反模型，（可能非适点）范畴;（ii）组合代数的斯通式表示定理;（iii）证明没有有效的Eudda模型可以有Euda-beta或Euda-beta-eta作为其方程理论（这可以被看作是对Honsell-Ronchi Della Rocca在1984年提出的一个开放问题的部分回答）。
2009-04-30 cs.LO
Extensional Models of Untyped Lambda-mu Calculus
本文提出了非类型λ-μ演算的新的数学模型。一种称为流模型，它是lambda模型的扩展，其中每个项都被解释为从流到单个数据的函数。另一类是流组合代数，它是组合代数的推广，证明了Lambda-mu演算的推广等式等价于流组合代数中的等式.为了定义流组合代数，我们引入了一个组合演算SCL，它是一个对应于Lambda-mu演算的无抽象系统。此外，它表明，流模型的代数特征为一类特殊的流组合代数。
2012-10-11 cs.LO
Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
受最近基于线性逻辑技术的λ演算的图形化形式的启发，我们引入了一种无类型的结构λ演算，称为λ j，它将距离上的动作与指数规则相结合，通过弱化、收缩和消除来分解替换.首先，我们证明了一些基本性质的lambda j，如合流和保存的β-强规范化。第二，我们添加了一个强大的互模拟λ j通过一个方程的理论，特别是捕获Regnier的西格玛等价。然后，我们完成了这两个以上的方程的互模拟（去）组成的替代品，我们证明，由此产生的演算仍然保持β-强规范化。最后，我们讨论了我们的结果的一些后果。
2012-03-23 cs.LO
On Coupled Logical Bisimulation for the Lambda-Calculus
我们研究了耦合逻辑互模拟（CLB）的原因上下文等价的演算。CLB起源于Dal Lago，Sangiorgi和Alberti的工作，作为一种工具来推理具有概率结构的微积分。我们适应原来的定义，以纯粹λ演算。我们开发了CLB的元理论，在按名称调用和按值调用中，并与应用互模拟（由于Abramsky）和逻辑互模拟（由于Sangiorgi，Kobayashi和Sumii）进行比较。我们还研究了增强的互模拟方法CLB开发的理论上的技术的情况下，对应于互模拟的功能不一定是单调的。
2014-10-10 cs.LO
A Rewriting Theory for Quantum Lambda-Calculus
本文针对量子lambda演算缺乏重写理论的问题，借助概率重写理论的新进展，重点研究并确立了其标准化与规范化结果。
2025-01-27 cs.LO
Semantics of a Typed Algebraic Lambda-Calculus
代数代数演算已经以各种方式进行了研究，但它们的语义大多未被触及。本文给出了一个具有向量空间结构的一般单型λ演算的语义分析。我们用两个已建立的向量代数演算来描述这种关系。然后我们研究了不动点组合子的加法所引起的问题以及如何修正方程理论来解决这些问题。我们勾勒出一个代数矢量PCF和它可能的指称解释。
2010-06-08 cs.LO
A recursive normalizing one-step reduction strategy for the distributive lambda calculus
我们肯定地回答了J. Klop的“Ustica Notes”中的问题A.1.6：“微$λ$ -演算是否有递归的归一化一步归约策略？“微$λ$ -演算是指由于Revesz的$λ$ -演算的实现，通过“微步骤”递归地将$β$ -redex $(λx.M)\ N$分布在其主体$M$上来实现$β$ -约简。
2014-04-30 cs.LO
Light Logics and the Call-by-Value Lambda Calculus
所谓的轻逻辑已经被引入作为具有相当显著的规范化性质的逻辑系统。然而，从这些逻辑为纯λ演算设计类型分配系统是有问题的。在本文中，我们表明，从通常的按名称调用的转换到按值调用的λ演算允许恢复与底层逻辑的强连接。这将在基本仿射逻辑（EAL）的上下文中完成，设计一个自然演绎风格的类型系统，将EAL公式分配给lambda项。
2008-11-07 cs.LO
Categorical Models for a Semantically Linear Lambda-calculus
本文是关于一个非常简单的语义线性λ演算的范畴化建模方法，命名为Sll演算。这是程序设计语言SlPCF的核心演算。特别是，在这项工作中，我们引入了Sll类的概念，这是能够描述一个非常大的类Sll演算的声音模型。Sll-范畴是对Benton、Bierman、Hyland和de Paiva的线性范畴的自然扩展，目的是为了更好地解释Sll-演算的所有结构。这个范畴足够一般，可以在Scott Domain和Coherence Spaces中捕捉有趣的模型。
2010-03-29 cs.LO
Nominal Coalgebraic Data Types with Applications to Lambda Calculus
我们研究了标称集上的最终余代数。这允许我们定义具有绑定的无限数据类型，所有构造都自动遵守alpha等价。我们给出了无穷λ演算的应用。
2013-12-09 cs.LO
A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract)
给出了按值调用线性λ演算的范畴语义。这种λ演算被塞林格和Valiron用作量子计算的函数式程序设计语言的主干。这个λ演算的一个特性是它的线性类型系统，它包括一个可重复性操作符“！“就像线性逻辑一样另一个主要特性是它的按值调用减少策略，以及对概率测量建模的副作用。“！“运算符产生一个comonad，如Seely，Bierman和Benton的线性逻辑模型。副作用产生了单子，就像莫吉的计算λ演算。这是一个单子和一个comonad的组合，使本文件有趣。我们表明，我们的范畴语义是健全的和完整的。
2008-01-05 cs.LO
The untyped stack calculus and Bohm's theorem
栈演算是一种函数式语言，它与经典逻辑具有Curry-Howard对应关系。它享有汇合，但以及帕里戈的fromda-mu，不承认玻姆定理，典型的fromda-calculus。我们提出了一个简单的扩展堆栈演算这是堆栈演算Saurin的λ-μ是λ-μ。
2013-03-29 cs.LO
The Vectorial Lambda Calculus Revisited
我们重新讨论向量λ演算，它是线性的类型化版本。向量（以及线性）最初是为量子计算设计的，作为系统F的扩展，其中lambda项的线性组合也是项，类型的线性组合也是类型。在其第一个演示中，Vectorial只提供了Subject Reduction属性的弱化版本。我们证明了我们修改后的向量λ演算支持标准版本的属性，回答了一个长期存在的问题。此外，我们还引入了类型权和项权的概念，并证明了项权与其类型权之间的关系。
2021-05-14 cs.LO
Superdeduction in Lambda-Bar-Mu-Mu-Tilde
超级演绎是一种专门设计的方法，以简化谓词逻辑中一阶理论的使用。运用这一理论，以系统、正确、完整的方式，用新的演绎规则丰富演绎体系。一个证明项语言和一个切消约化已经存在于超演绎中，两者都是基于克里斯蒂安·厄本在经典微积分上的工作。然而，克里斯蒂安·厄本的微积分的计算内容与柯里-霍华德对应（Curry-Howard correspondence）没有直接关系。相反，Lambda bar mu mu波浪线演算是经典波浪线演算的一种波浪线演算。这个简短的文件是第一步，进一步探索的计算内容的superdeduction证明，我们延长了Lambda酒吧亩亩波浪演算，以获得一个proofterm语言一起削减消除减少superdeduction。我们还证明了强大的规范化，这种扩展的λ酒吧亩亩波浪演算。
2011-01-28 cs.LO
Universal Semantics for the Stochastic Lambda-Calculus
我们为随机λ演算定义了合理的和充分的指称和操作语义。这两种语义方法建立在以前的工作，使用类似的技术来推理高阶概率程序，但第一次承认一个充分性定理有关的操作和指称的意见。这解决了（Bacci等人，2018）中未解决的主要问题。
2021-05-14 cs.LO
Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)
lambda Pi演算可以通过重写规则来扩展，以嵌入任何函数式纯类型系统。在本文中，我们证明了嵌入是保守的，通过证明一个相对形式的规范化，从而证明使用的lambda Pi演算模重写作为一个逻辑框架的逻辑基于纯类型系统。这个结果以前只在目标系统是标准化的条件下得到证明。我们的方法不依赖于这个条件，因此在源系统未归一化时也有效。
2015-04-21 cs.LO
Intersection Types for the Computational lambda-Calculus
我们研究多态类型分配系统的非类型的的影响，基于Moggi的单子方法。从单子的抽象定义出发，我们引入了一个基于Wadler的变体的按值调用的计算型微积分，该变体具有单元和绑定组合子，并且没有let。我们定义了一个概念，减少演算，并证明它是合流的，我们也涉及到我们的演算的原始工作的莫吉表明，他的无类型的元语言可以解释和模拟在我们的演算。然后，我们介绍了一个交集型系统启发Barendregt，Coppo和Dezani系统的普通λ演算，建立转换下的类型不变性，并通过逆极限和过滤器模型的构造提供了演算的模型，并将它们联系起来。我们证明了类型系统的可靠性和完备性，以及主题缩减和扩展属性。最后，我们引入了一个收敛的概念，这是完全相关的减少，并通过其类型的收敛项的特征。
2020-02-07 cs.LO
A Symmetric Lambda-Calculus Corresponding to the Negation-Free Bilateral Natural Deduction
Filinski构建了一个对称的λ演算组成的表达式和延续是对称的，和功能，具有对偶性。在他的微积分中，函数可以使用原始运算符编码为表达式和延续。也就是说，函数的对偶性不是在微积分中推导出来的，而是作为微积分的一个原理而被采用的。在本文中，我们提出了一个简单的对称的λ演算对应的否定自由自然演绎的双边证明论语义。在我们的微积分中，连续类型不是表示为公式的否定，而是表示为具有负极性的公式。函数类型在直觉逻辑和次协调逻辑中分别表示为蕴涵和非但连接词。我们的演算不仅简单，而且功能强大，因为它包括与Wadler发明的按值调用二元演算相对应的调用值演算。我们表明，表达和延续之间的相互转换是可定义的，在我们的微积分证明的对偶功能。我们还证明了每个可类型函数都有对偶类型。因此，功能的二重性来源于双边主义。
2021-01-29 cs.LO
A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
我们描述了一个类型系统的线性代数λ演算。类型系统解释了语言中模拟线性运算符和向量的部分，也就是说，它能够静态地描述程序归约所产生的项的线性组合。这就产生了一个原始的类型论，在这个理论中，类型可以像项一样叠加成线性组合。我们表明，所得到的类型的λ演算是强规范化和功能弱主题减少。
2012-07-31 cs.LO
Pattern Unification for the Lambda Calculus with Linear and Affine Types
我们定义了模式片段的高阶统一问题的线性和仿射类型论，并给出了一个确定性的统一算法，计算最一般的统一。
2010-09-14 cs.LO
Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus
我们研究了通过两个交换规则（sigma-reductions）的Plotkin的呼叫按值计算λ演算的扩展。这些交换规则足以从演算中去除有害的按值调用范式，因此它享有许多语义属性的优雅特征。我们证明了这个扩展的演算是一个保守的改进Plotkin的。特别是，这个演算的可解性和潜在价值性的概念与Plotkin的按值调用λ演算相吻合。证明依赖于一个标准化定理证明了推广高桥的方法，并行减少我们的一套减少规则。标准化是弱的（即，赎回没有完全序列化），因为减少之间的重叠干扰。
2017-12-21 cs.LO
The Undecidability of Typability in the Lambda-Pi-Calculus
该研究证明λΠ-演算中给定语境下可类型化纯项集非递归，得出编程语言Elf无通用类型推断算法、部分场景需程序员标注类型信息的结论。
2023-06-13 cs.LO
Confluence via strong normalisation in an algebraic λ-calculus with rewriting
线性-代数演算和代数演算是用任意线性组合项扩展的无类型代数代数演算。前者以重写系统的形式呈现线性代数的公理，而后者使用等式。当重写时，代数演算不是融合的，除非增加进一步的限制。我们提供了一个类型系统的线性代数演算强制执行强规范化，这给回汇合。类型系统允许在系统F中进行抽象解释。
2012-03-28 cs.LO
A Tutorial Introduction to the Lambda Calculus
这篇文章是对$λ$ -演算的一个简明而轻松的介绍。这种形式主义是由Alonzo Church开发的，作为研究有效可计算函数的数学性质的工具。形式主义变得流行起来，并为函数式程序设计语言家族提供了强大的理论基础。本教程展示了如何使用$λ$ -演算执行算术和逻辑计算，以及如何定义递归函数，即使$λ$ -演算函数是未命名的，因此不能显式地引用它们自己。
2015-03-28 cs.LO
Embedding Pure Type Systems in the lambda-Pi-calculus modulo
本文证明通过添加计算规则扩展的 lambda-Pi-calculus modulo 具有惊人表达能力，可将系统 F 等函数式 Pure Type Systems 保守嵌入其中。
2023-10-19 cs.LO
Lambda Calculus with Explicit Read-back
本文介绍了一种新的长期重写系统，这是类似于嵌入式读回机制的互动网络在我们以前的工作，但更容易遵循比在原来的设置，从而分析其属性。也就是说，我们验证了它正确地代表了λ演算。此外，我们表明，有一个减少序列，在我们的长期重写系统中的任何一项开始。最后，我们代表了最左边的策略，这是已知的正常化。
2018-08-20 cs.LO
Termination of lambda-calculus with the extra Call-By-Value rule known as assoc
在本文中，我们证明了任何一个强正规化的β-减少的β-长期也是强正规化的β，assoc-减少。ascloud是一种按值调用规则，已在Moggi，Joachimsky，Escherichto Santo和其他人的作品中使用。其结果往往是合理的不完整或不正确的证明。在这里，我们给出一个完整的细节。
2008-09-02 cs.LO
Two linearities for quantum computing in the lambda calculus
我们提出了一种方法来统一量子代数演算中的两种非克隆方法：逻辑线性和代数线性。第一种方法是禁止重复变量，而第二种方法是将所有的非线性项都视为代数线性函数。我们通过定义一阶简单类型的量子扩展来说明这个想法，其中类型在叠加上是线性的，同时允许克隆基向量。此外，我们提供了一个解释的演算叠加类型被解释为向量空间和非叠加类型作为其基础。
2019-07-31 cs.LO
Standardization in resource lambda-calculus
资源演算是允许对资源消耗建模的λ演算的扩展。它本质上是非确定性的，有两个一般的归约概念-一个是并行的，保留所有可能的结果作为正式的总和，另一个是非确定性的，在每一步都进行排他性的选择。我们证明了非确定性约简具有标准化的概念，这是经典λ演算中类似约简的自然推广。完全并行归约只是具有较弱的标准化概念。其结果允许一个操作表征可能的可解性，这已经介绍和特点（从语法和逻辑的角度来看）的帕加尼和Ronchi德拉罗卡。
2012-11-17 cs.LO
Rewriting Modulo βin the λΠ-Calculus Modulo
Modulo是一个依赖类型的Algorithm的变体，其中beta转换扩展了用户定义的重写规则。它是一个表达性的逻辑框架，并已被用于以浅层次的方式编码逻辑和类型系统。基本的性质，如主题归约或类型的唯一性，一般不适用于Muda-Pi-calculus Modulo。然而，如果由重写规则与β-归约一起生成的重写系统是汇合的，则它们成立。但这限制太多了。为了处理不融合来自于beta-约简和重写规则之间的干扰的情况，在它们的左手边，我们引入了重写模beta的概念，用于对beta-Pi-演算模进行重写。我们证明了重写模beta的汇合足以确保主题减少和类型的唯一性。我们通过将π演算模编码到高阶重写系统（HRS）中来实现我们的目标。因此，我们也使合流的结果，可用于HRSs的Pudda-Pi-演算模。
2015-07-29 cs.LO
Superdevelopments for Weak Reduction
我们研究了Cagman和Hindley的弱λ演算的超发展，这是标准弱λ演算的一个融合变体，其中禁止将λ演算还原到λ以下。与发展相反，从一个术语M的超发展不仅允许减少M中的赎回权的残差，而且还允许一些新创建的残差。在λ演算中，有三种方法可以创建新的redex;在弱λ演算中，一种新形式的redex创建是可能的。给出了弱λ演算超发展的标号约简公式和同时约简公式，并证明了它们的等价性.
2010-01-25 cs.LO
A Quick Overview on the Quantum Control Approach to the Lambda Calculus
在这个简短的概述中，我们从量子计算的基础知识开始，解释量子和经典控制范式之间的差异。我们给出了一个概述的量子控制线的研究范围内的λ演算，从无类型的演算到分类和realisability模型。这是对过去10多年来这一领域研究的总结，从Arrighi和Dowek的开创性工作开始直到今天。
2022-04-08 cs.LO
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
A new coinductive confluence proof for infinitary lambda calculus
本文提出了无穷λ演算中Böhm归约合流性与规范化的新余归纳证明，该证明更简单且技术新颖，并在Coq中形式化验证。
2020-03-10 cs.LO
A fully-abstract semantics of lambda-mu in the pi-calculus
我们研究了Muda-mu演算，扩展与明确的替代，并定义了一个组合输出为基础的解释到一个变种的π演算与配对，保留单步显式头减少弱双相似性。我们定义了四个概念的弱等价的Euda-mu-一个基于弱约化，两个建模弱头约化和弱显头约化（所有考虑没有弱头范式等价项），和一个基于弱近似-并显示它们都是一致的。然后，我们将展示完整的抽象结果，我们的解释弱等价弱双相似的过程。
2014-09-11 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
The lambda-mu-T-calculus
带有控制算子的微积分作为简单类型论的扩展而被研究。真正的程序设计语言包含数据库，因此要真正理解控制运算符，还应该在演算中包含这些。作为朝这个方向迈出的第一步，我们引入了Parigot的Mu-演算和Gödel的T的组合-Mu-T，以扩展具有自然数数据类型的控制算子的演算，并使用原始递归。我们考虑的问题，汇合的原始条款，以及强规范化的良好类型的条款。观察一些问题，延长证明巴巴等人。和Parigot的原始汇合证明，我们提供了新的，改进的，证明汇合（通过完整的发展）和强规范化（通过reductionary和推迟参数）为我们的系统。最后，我们对改进演示的扩展、选择和前景进行了一些评论。
2012-04-02 cs.LO
A Typing System for the Linear Lambda-Calculus in de Bruijn Notation
LORIA, UMR 7503, Université de Lorraine, CNRS, Inria（洛林大学、法国国家科学研究中心、法国国家信息与自动化研究所）
研究为德布鲁因记号下的线性λ演算引入适合的类型系统，其规则类似霍达斯和米勒模型，能保证项的线性且无需出现检查，还确立了归约主题性质。
2026-07-23 cs.LO
(Towards a) Statistical Probabilistic Lazy Lambda Calculus
本文研究了统计概率编程语言模型的需求，提出通过结合开放互模拟和概率模拟等传统工具即可满足这些需求。
2024-03-22 cs.LO
Substitution in the lambda Calculus and the role of the Curry School
本文探讨了lambda演算中替换与alpha同余的相互依赖问题，指出Curry学派的研究优雅地解决了这一让学生困惑的难题，以此颂扬其在替换与alpha同余领域的贡献。
2024-01-05 cs.LO
Clone Theory: Its Syntax and Semantics, Applications to Universal Algebra, Lambda Calculus and Algebraic Logic
本文的主要目的是提出一种统一的方法，将逻辑系统的语法转化为一定的初始代数结构，以便用代数的方法来研究它。为此目的人们可以选择的代数结构是一个范畴的一个完整子范畴上的各种克隆。证明了方程逻辑、λ演算和一阶逻辑的语法都可以表示为正整数集合上的克隆或克隆的右代数。语义，然后表示来自这些克隆左代数的结构。
2008-10-17 cs.LO
Interpreting Lambda Calculus in Domain-Valued Random Variables
Heriot-Watt University（赫瑞-瓦特大学）；McGill University（麦吉尔大学）；Carnegie Mellon University（卡内基梅隆大学）
研究如何用域值随机变量解释λ演算，核心方法是发展布尔值域理论并聚焦自反域构造，主要贡献是给出在布尔代数中解释相等性概念及方程有效性的方式。
2026-07-09 cs.LO
A call-by-value lambda-calculus with lists and control
微积分与控制运营商已被研究的原因控制程序设计语言和解释经典证明的计算内容。为了使这些演算成为真正的程序设计语言，还应该包括数据类型。作为向这个方向迈出的一步，本文定义了一个简单类型的按值调用λ演算，它具有控制操作符catch和throw、列表的数据类型和用于原语递归的操作符（类似于Goedel的T）。我们证明了我们的系统满足主题减少，进步，合流无类型的条款，以及良好的类型条款的强规范化。
2012-10-11 cs.LO
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
一个新的，全面的方法来解决居住问题的简单类型的λ演算，处理决策和计数问题。这种方法的工作原理是利用一个表示的搜索空间所产生的一个给定的居住问题，这是在一个证明搜索，作者最近开发的微积分。这种表示可以被看作是通过类元项扩展证明的Curry-Howard表示，保持在λ演算和类型系统的方法内。我们的方法揭示了归纳描述的决策问题，由证明搜索表达式的语法驱动，最终产品是简单的，递归的决策程序和计数功能。
2017-03-11 cs.LO math.LO
Lambda Calculus and Probabilistic Computation
我们介绍了两个扩展的$λ$演算的概率选择操作，$Λ_\oplus^{cbv}$和$Λ_\oplus^{cbn}$，分别按值调用和按名称调用概率计算。我们证明，都享有合流和标准化，在一个扩展的方式：我们重新审视这两个基本概念，考虑到渐近行为的条款。这两种演算的共同根源是基于线性逻辑的进一步演算，$Λ_\oplus^!$，它允许对选择和复制之间的交互进行精细控制，并允许我们开发统一的模块化方法。
2019-05-10 cs.LO
Full Abstraction for a Recursively Typed Lambda Calculus with Parallel Conditional
我们定义了一个递归类型的λ演算的语法和约简关系，并给出了一个并行的条件函数。减少显示为融合性。我们将递归类型解释为受限形式的信息系统，我们称之为素系统。一个指称语义定义与此解释。定义了项的语法范式逼近，证明了逼近定理：项的语义等于其逼近的语义的极限。证明使用包含谓词（逻辑关系）。对于布尔值的观察，语义是足够的。在平行格功能的存在下，它也是完全抽象的。
2008-06-11 cs.LO
An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus
本文汇集了两条线的研究：隐式表征的复杂性类的线性逻辑（LL）的一方面，计算在一个任意的环上的Blum-Shub-Smale（BSS）模型的另一方面。给定一个固定的环结构K，我们定义了一个扩展的Terui的轻仿射λ演算类型的LAL（轻仿射逻辑）与K的基本类型。我们表明，这种演算捕获的多项式时间函数类FP（K）：每个类型的长期可以评估在多项式时间，相反，每一个多项式时间BSS机在K可以模拟在这种演算。
2006-08-08 cs.LO
Macro Lambda Calculus
我们的宏λ演算项目（MLC）的目标是将λ项编码到交互网络中。它的软件实现将接受类似于允许宏定义的λ演算的符号输入。输出类似于交互演算，适用于我们的交互网络计算程序（INC）。在本文中，我们描述了按需调用评估的交互系统和编码的机制，在这个系统中的lambda条款MLC是基于。
2015-08-07 cs.FL cs.LO
Strict Ideal Completions of the Lambda Calculus
Kennaway等人开创的无限λ演算通过度量完备化将基本λ演算扩展到无限项和约简。根据所选择的度量，所得到的无穷演算表现出不同的严格性概念。为了获得这些结石的无穷规范化和无穷融合特性，Kennaway等人用无限多个“$\bot$ -规则”扩展了$β$ -归约，这些规则将无意义的项直接收缩为$\bot$。三个由此产生的Böhm约化演算具有唯一的无穷范式对应的Böhm类树。在本文中，我们发展了一个相应的理论，无限lambda演算的理想完成，而不是度量完成的基础上。我们表明，我们的每一个演算保守地扩展了相应的基于度量的演算。我们的三个演算是无穷正规化的和融合的;它们唯一的无穷范式正好是相应的基于度量的演算的类波姆树。我们的演算免除了基于度量的演算的无穷多个$\bot$ -规则。完全非严格演算（称为$111$）仅由$β$ -归约组成，而另外两个演算（称为$001$和$101$）需要两个额外的规则来精确地说明它们的严格性属性：$λx.\bot \to \bot$（用于$001$）和$\bot\,M \to \bot$（用于$001$和$101$）。
2018-05-17 cs.LO
The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi
λ演算中对绑定的内在处理使其成为一种理想的数据结构，用于表示具有绑定的语法对象，如公式、证明、类型和程序。在实现中支持这样的数据结构由于相对于λ项的替换操作的复杂性而变得困难。在本文中，我们提出了悬浮演算，明确处理Meta级绑定的λ演算。我们证明这个演算的性质，使它成为一个合适的替代λ演算的实施。最后，我们比较了悬浮演算与其他显式处理的替代。
2007-02-05 cs.LO cs.PL
Light types for polynomial time computation in lambda-calculus
本文提出了一种新的类型系统：对偶轻仿射逻辑（DLAL），它保证了类型良好的程序可以在多项式时间内执行。DLAL有一个简单的类型语言，带有线性和直观的类型箭头，以及一个模态。它对应于光仿射逻辑（LAL）的一个片段。我们表明，相反的LAL，DLAL确保良好的性能上的主题减少是满意的，一个良好的类型的长期承认多项式约束的减少任何策略。我们建立，作为LAL，DLAL允许代表所有的多时间功能。最后给出了命题DLAL的一个类型推断过程。
2004-05-11 cs.LO
Labelled Lambda-calculi with Explicit Copy and Erase
我们提出了两个重写系统，定义标记显式替换的Alzoda-calculi。我们的工作是出于Levy的标记的代数演算和证明网中的路径之间的密切对应关系，这在相互作用几何的理解中发挥了重要作用。标签的结构在利维的标记的Bendida演算涉及到路径的乘法信息，我们的工作的新颖性是，我们设计的标记明确的替代演算，也保持跟踪指数信息存在于呼叫的按值和呼叫的Bendida演算到线性逻辑证明网的名称翻译。
2010-03-29 cs.LO
