Proof nets and the call-by-value lambda-calculus
本文详细介绍了按值调用λ演算（的一种变体）与线性逻辑证明网之间的关系。为了实现两个系统之间的强互模拟，我们对演示进行了仔细的调整：微积分上的每一个重写步骤都映射到网络上的单步的，反之亦然。通过这种方式，我们得到了证明网的代数重构。此外，我们为我们的证明网提供了一个简单的正确性标准，它以一种不寻常的方式使用盒子。
2013-03-29 cs.LO cs.PL
From Semantics to Types: the Case of the Imperative lambda-Calculus
我们提出了一个交叉型系统的一个强制性的基于状态单子和代数运算的演算读取和写入存储。该系统是通过求解一个合适的域方程的欧米茄代数格的范畴;该解决方案包括一个过滤器模型推广了著名的建设普通的λ演算。然后，类型系统从过滤器模型本身的术语解释中获得。这样得到的类型系统满足“类型语义”属性，并且通过构造它是可靠的和完备的。
2021-12-28 cs.LO cs.PL
Decomposing Probabilistic Lambda-calculi
概率演算的概念通常带有一个规定的归约策略，通常是按名称调用或按值调用，因为演算是非融合的，这些策略会产生不同的结果。这是一个突破的主要优势之一，微积分：融合，这意味着结果是独立于战略的选择。我们提出了一个概率的概率运算符分解成两个语法结构：一个发电机，它代表一个概率事件;和消费者，它的行为取决于一个给定的事件的条款。由此产生的演算，概率事件Lambda演算，是融合的，并解释调用的名称和调用的值策略，通过不同的解释概率运算符到我们的生成器和消费者结构。我们提出了两个概念的减少，一个通过细粒度的本地重写步骤，和一个通过生成和消费的概率事件。演算的简单类型基本上是标准的，它们传达了强规范化。我们演示了如何编码按名称调用和按值调用的概率评估。
2020-02-19 cs.LO cs.PL
Probabilistic Operational Semantics for the Lambda Calculus
研究了纯λ演算的非确定性扩展的概率操作语义.在这种语义中，一个项计算为（有限或无限）值分布。小步和大步语义都是归纳和共归纳定义的。此外，小步和大步语义产生相同的结果，无论是在调用的值和调用的名称。Plotkin的CPS翻译进行了扩展，以适应选择操作符和正确的操作语义。最后，所得到的系统的表达能力进行了研究：微积分是健全的和完整的可计算的概率分布。
2011-06-27 cs.LO cs.PL
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
我们正式验证一个抽象的机器调用的值的alcuda演算与de Bruijn条款，简单的替代，和小步语义。我们遵循逐步改进的方法，从一个带有替换的朴素堆栈机器开始。然后，我们细化到一个具有闭包的机器，最后是一个具有为闭包提供结构共享的堆的机器。我们证明了三个细化步骤的正确性与组成小步自下而上的模拟。有一个附带的Coq开发验证所有结果。
2019-01-02 cs.LO cs.PL
On the confluence of lambda-calculus with conditional rewriting
无类型λ演算与无条件重写的融合已经在各个方向上进行了研究。本文研究了λ演算与条件重写的融合问题，并给出了两个方向的一般结果。首先，当条件规则是代数的时候。这扩展了Muller和Doughnard关于无条件重写的结果。考虑两种情况，在条件评估中是否允许β-还原。同时，将Doughnard的结果从强正规化β-约简的假设改进为弱正规化β-约简的假设.我们还提供的例子表明，在这些条件之外，模块化的融合是难以实现的。其次，我们超越了代数框架，并得到新的汇合结果，使用扩展的概念，利用重写规则的条件部分的正交性。
2006-09-11 cs.LO cs.PL
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
我们研究了一类简单类型的λ演算的名义代数Henkin式模型，其中变量映射到表示中的名称，而λ演算抽象映射到（非功能性的）名称抽象操作。由此产生的表示更小，更好的行为，在我们精确的方式，比基于函数值的模型。使用这些新的模型，我们然后开发了一个概括的λ-长期语法丰富他们的存在元变量，从而产生一个理论的不完整的功能。这种不完备性与函数抽象和应用给出的不完备性的通常概念是正交的，并且对应于洞和不完备对象。
2011-11-01 cs.LO cs.PL
Encoding Turing Machines into the Deterministic Lambda-Calculus
这篇笔记是关于将图灵机编码到λ演算中的。
2017-11-28 cs.LO
On Constructor Rewrite Systems and the Lambda-Calculus (Long Version)
我们证明了正交构造函数项重写系统和弱（即，在可编程抽象的范围内不允许减少）按值调用减少可以用线性开销来相互模拟。特别地，弱按值调用beta归约可以通过正交构造器项重写系统以相同数量的归约步骤来模拟。相反，术语重写系统中的每个约简可以通过恒定数量的β约简步骤来模拟。这与隐式计算复杂性有关，因为在弱按值调用约简下，范式的beta步骤的数量与规范化的实际成本（即，在图灵机上执行的）多项式相关。因此，正交构造函数项重写系统和λ演算都与图灵机多项式相关，将其自然参数作为成本的概念。
2012-08-02 cs.LO cs.PL
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
An Introduction to the Clocked Lambda Calculus
我们简要介绍了时钟λ演算，一个扩展的经典λ演算与一元符号τ用于见证β步骤。与经典的λ演算相比，这种推广是无穷强正规化的和无穷汇合的。无限范式是丰富的Boehm树，我们称之为钟控Boehm树。
2014-05-29 cs.LO
Relational Parametricity and Control
我们研究了Parigot的二阶微积分的方程理论，并将其转换为二阶微积分的一个片段。据观察，目标演算上的关系参数诱导一个自然的概念等价的-条款。另一方面，无约束的关系parametricity的演算原来是不一致的CPS语义。根据这些事实，我们建议以一种受约束的方式在微积分上制定关系参数，这可能被称为“焦点参数”。
2006-07-27 cs.LO cs.PL
Intersection Types for a Computational Lambda-Calculus with Global State
本文研究带全局存储读写操作的无类型 lambda 演算，利用 monad 建模副作用，建立操作语义、指称语义与交集类型系统，并证明类型不变性及收敛项的类型刻画。
2025-08-27 cs.LO cs.PL
Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS
我们以前已经出版了Isabelle/HOL形式化的一般理论的语法绑定。在这篇配套文件中，我们实例化的一般理论，以语法的λ演算和形式化的发展，导致几个基本的结构和结果：健全的语义解释，教会罗瑟和标准化定理，高阶抽象语法（HOAS）编码。对于Church-Rosser和标准化，我们的工作涵盖了微积分的按名称调用和按值调用版本，遵循Takahashi和Plotkin的经典论文。在形式化过程中，我们能够专注于开发的高级思想-感谢我们的一般理论提供的武器库：关于替换，交换和新鲜度操作符的丰富基本事实，以及递归定义和推理原则，包括语法语义解释的专业化。
2021-07-24 cs.LO cs.PL
Lecture notes on the lambda calculus
这是一组课堂讲稿，是我2001年在渥太华大学，2007年和2013年在达尔豪西大学教授的λ演算课程的基础上发展起来的。这些笔记涵盖的主题包括无类型λ演算、Church-Rosser定理、组合代数、简单类型λ演算、Curry-Howard同构、弱规范化和强规范化、多态性、类型推断、指称语义、完全偏序和PCF语言。
2013-12-26 cs.LO
Expressibility in the Lambda Calculus with Letrec
我们调查之间的关系，有限项的Lenda-letrec，与letrec的λ演算，和无限的lambda条款，他们表示。由于有一些简单的例子，λ-项，直观上，是不是展开的条款在λ-letrec，我们考虑的问题：如何可以这些无限的lambda条款的特点是λ-letrec-表达的意义上，他们可以获得无限展开的条款在λ-letrec？为了通过在项的头部进行的重复“实验”来“观察”无限的子项，我们引入了两个重写系统（具有重写关系）-reg->和-reg+->，它们分解项，并在两个概念中产生“生成的子项”。因此，可以观察步骤的种类以及其目标，生成的子项。在这两个系统中，都有四种分解步骤：-lambda-> steps（分解一个抽象），-@0>和-@1> steps（将应用程序分解为它的函数和参数），以及-del-> steps（定义抽象的作用域，对于-reg->）和-S->（定义作用域，对于-reg+->）。这些步骤发生在无限的抽象项上，这些抽象项带有一个前导前缀，用于收集以前遇到的抽象项，并保持生成的子项关闭。我们称一个无限的可达项为“正则”/“强正则”，如果它的-reg-> -reachable / -reg-> -reachable生成子项的集合是有限的。此外，我们还用“结合-捕获链”的概念分析了非线性项的结合结构。使用这些概念，我们回答了上面的问题，提供两个特征的可表达性。对所有无穷多项M…
2013-05-02 cs.LO cs.PL
A Categorical Model for the Lambda Calculus with Constructors
带构造函数的λ演算是带变元构造函数的λ演算的扩展。它将ML模式匹配分解为对常量的实例分析和实例与应用构造之间的交换规则。虽然这种交换规则与通常的计算直觉不匹配，但它使微积分具有表达性和融合性，语法相当简单。本文对带构造函数的λ演算定义了一个合理的范畴模型概念。然后，我们证明了这个定义是完整的片段的演算没有匹配失败，使用模型的部分等价关系。
2012-03-05 cs.LO
Hereditary Substitution for the λΔ-Calculus
遗传替换是类型有界迭代替换的一种形式，首先由沃特金斯等人和亚当斯明确提出，以显示各种构造性逻辑的证明项的规范化。本文是第一个应用遗传替代显示规范化的类型论对应于一个非建设性的逻辑，也就是说，三角洲演算制定的Zeroof。我们证明了简单类型的λ演算的遗传替换函数有一个非平凡的扩展到一个的λ-Delta演算。然后用遗传替换证明了归一化。
2013-09-05 cs.LO cs.PL
RPO, Second-order Contexts, and Lambda-calculus
首先，我们扩展了Leifer-Milner RPO理论，给出了获得IPO标记的过渡系统（和双相似性）的一般条件，减少了一组过渡，并可能出现分支。此外，我们还研究了Leifer-Milner理论的弱变体，给出了弱双相似是同余的一般条件。然后，我们将这种扩展的RPO技术应用到具有懒惰和按值调用的Reduction策略的λ演算中。我们表明，相反的过程演算，可以直接处理的λ演算语法和应用Leifer-Milner技术一类的背景下，只要我们的工作框架中的弱双相似性。然而，即使在具有最小上下文的转换系统的情况下，所得到的双相似性也是无限分支的，这是因为在标准上下文范畴中，参数规则（如beta规则）只能由无限多个基本规则表示。为了克服这个问题，我们引入了二阶上下文范畴的一般概念。我们表明，通过在这种情况下进行RPO建设，懒惰的观测等价可以被捕获为一个弱的双相似等价的一个分支过渡系统。这个结果是通过考虑组合逻辑中的一种编码来实现的。
2009-08-06 cs.LO cs.PL
Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion
我们研究的语义资源敏感的扩展的λ演算在一个典型的自反对象的一个类别的集合和关系，斯科特的原始模型的纯λ演算的关系版本。这种演算与Boudol的资源演算有关，并且是从线性逻辑的Ehrhard和Regnier的微分扩展和λ演算导出的。我们扩展它与新的建设，被理解为实现一个非常简单的异常机制，并与“必须”并行组合。这些新的操作允许将该演算的上下文与模型的任何点相关联，并证明对于有限子演算的完全抽象，其中普通的λ演算应用是不允许的。然后通过泰勒展开公式将结果推广到全微积分。作为中间结果，我们证明了例外机制是不必要的有限子演算。
2012-10-08 cs.LO
Counting and Generating Terms in the Binary Lambda Calculus (Extended version)
在一篇名为Binary λ演算and combinatory logic的论文中，John Tromp提出了一种将λ演算项编码为二进制序列的简单方法。在下面的内容中，我们研究了表示lambda项的给定大小的二进制字符串的数量，并从它们的生成函数中得出结果，特别是大小为n的项的数量大致增长为1.963447954。.. n.在第二部分中，我们使用这种方法来生成随机lambda项使用玻尔兹曼采样器。
2015-11-17 cs.LO
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
一个新的，全面的方法来解决居住问题的简单类型的λ演算，处理决策和计数问题。这种方法的工作原理是利用一个表示的搜索空间所产生的一个给定的居住问题，这是在一个证明搜索，作者最近开发的微积分。这种表示可以被看作是通过类元项扩展证明的Curry-Howard表示，保持在λ演算和类型系统的方法内。我们的方法揭示了归纳描述的决策问题，由证明搜索表达式的语法驱动，最终产品是简单的，递归的决策程序和计数功能。
2017-03-11 cs.LO math.LO
Semantics of Typed Lambda-Calculus with Constructors
我们提出了一个Curry风格的二阶类型系统，具有并集和交集类型的Arbiser，Miquel和Rios的构造器的λ演算，扩展的λ演算与可变构造器的模式匹配机制。然后，我们证明了强规范化和匹配失败的限制，这个系统的情况下，通过适应标准的reductionmethod。
2011-03-16 cs.LO
Graphic lambda calculus and knot diagrams
在arXiv：1207.0332 [cs.LO]中提出了一种图形lambda演算形式，它具有对应于无类型lambda演算和涌现代数的扇区。在这里，我们探讨部门覆盖结图，这是作为宏构建在图形lambda演算。
2012-11-07 cs.LO math.GT math.LO
Confluence Results for a Quantum Lambda Calculus with Measurements
证明了带测量的量子微积分Q* 的一个强收敛结果。更准确地说，合流举行有限和无限的计算。融合证明中使用的技术是语法上的，但具有创新性。这使得Q* 不同于类似的量子lambda演算，后者要么是无测量的，要么是提供了一个约简策略。
2009-05-28 cs.LO
Macro Lambda Calculus
我们的宏λ演算项目（MLC）的目标是将λ项编码到交互网络中。它的软件实现将接受类似于允许宏定义的λ演算的符号输入。输出类似于交互演算，适用于我们的交互网络计算程序（INC）。在本文中，我们描述了按需调用评估的交互系统和编码的机制，在这个系统中的lambda条款MLC是基于。
2015-08-07 cs.FL 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
An Elementary Fragment of Second-Order Lambda Calculus
定义了二阶λ演算（系统F）的一个片段，它刻画了初等递归函数.类型量化被限制为非交织和分层，即，这些类型被分配了级别，并且量化变量只能由级别较小的类型实例化，对级别零的处理稍微宽松。
2004-03-18 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
On graphic lambda calculus and the dual of the graphic beta move
这是一个简短的描述图形lambda演算，特别强调了一个二重性所建议的两个不同的外观结图，在lambda演算和紧急代数部门的图形lambda演算分别。这种二元性导致了图形贝塔移动的二元性的引入。虽然图形贝塔移动对应于无类型lambda演算中的贝塔约化，但对偶图形贝塔移动出现在与涌现代数有关的情况下。
2013-02-04 cs.LO math.GT math.LO
Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
我们给出了一个语义的λ演算的基础上的拓扑对偶定理的名义集。一个新的解释lambda给出的伴随，和lambda-条款绝对解释为集（没有估值是必要的）。
2016-10-06 cs.LO math.LO
Uniform Memory and Serialization for Lambda Calculus
本文介绍了一种特殊类型的系统，定义了它们的性质，并证明了纯无类型可拓λ演算的归约机可以实现为所介绍类型的系统。具体地说，我们讨论了作为一种特殊的图形的均匀记忆和实时的操作的状态机，使用均匀记忆作为他们的状态。此外，我们考虑一种特殊的串行化情况，后者对于在计算期间比较结果的机制很有用，而不是在计算完成之后。然而，我们首先详细解释我们这项工作的动机。
2010-11-16 cs.LO cs.PL math.LO
On Models of the Planar Lambda Calculus
University of Tartu（塔尔图大学）
本文通过构造伴随关系统一了平面Lambda演算的两种建模方法，并据此证明了平面版本的斯科特表示定理。
2026-09-16 cs.LO math.CT
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
On the discriminating power of tests in resource lambda-calculus
自发现以来，差分线性逻辑（DLL）启发了许多领域。在指称语义中，DLL的范畴模型已经比较普遍，其中最简单的是Rel，即集合和关系的范畴。在证明论中，这自然产生了完全和完整的DLL差分证明网。反过来，这些工具可以自然地转化为它们的直觉对应物。通过采取共同克莱斯利类别相关联的！comonad，Rel变成MRel，一个包含微分概念的\Lcalcul模型。证明网可以很自然地用于将\Lcalcul扩展为具有资源的λ演算，一种包含线性和微分概念的演算。当然，MRel是一个有资源的\Lcalcul模型，它已经被证明是足够的，但是它是完全抽象的吗？这是布恰雷利、卡拉罗、埃哈德和曼佐内托的一个强有力的猜想。然而，在本文中，我们展示了一个反例。此外，为了更直观地了解反例的本质并寻求更大的普遍性，我们将使用Bucciarelli等人也引入的资源\Lcalcul的扩展，其中$\Minf$是完全抽象的，即测试。
2012-05-22 cs.LO cs.PL
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
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
我们观察到，标准化评估简单类型的λ演算与弱余积可以进行在一个弱双carbohydrate封闭范畴的预层配备了单子，使我们能够执行的情况下区分中性条款的总和类型。单子的位置影响我们得到的范式：例如，把单子放在余积上，我们得到η长的β-π范式，其中π是指排除位置之外的格区别的排列。我们进一步观察到，将单子放在每一个联积上是相当浪费的，单子的最佳放置可以通过考虑受聚焦启发的极化简单类型来确定。极化将类型分为正类型和负类型，将正类型嵌入负类型时放置单子就足够了。我们考虑两个基于极化类型的演算：纯推值调用（CBPV）和极化的λ演算，自然演绎演算对应于聚焦递归演算。对于这两个结石，我们提出的算法进行规范化的评价。我们进一步讨论了不同的实现单子和它们的关系，现有的规范化证明的λ演算和。我们的发展已部分正式在阿格达证明助手。
2019-02-16 cs.LO cs.PL math.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
