Local and global moves on locally planar trivalent graphs, lambda calculus and $λ$-Scale
我们给出了一类局部平面三价图的局部和全局移动的描述，我们表明，它包含$λ$ -规模演算，因此，特别是无类型的λ演算。令人惊讶的是，β约化规则来自于三价局部平面图的局部“缝合”变换。
2012-07-02 cs.LO math.GT math.LO
Encoding Turing Machines into the Deterministic Lambda-Calculus
这篇笔记是关于将图灵机编码到λ演算中的。
2017-11-28 cs.LO
A concrete model for a typed linear algebraic lambda calculus
本文为带测量的类型化线性代数 lambda 演算 Lambda-S 构造了基于集合与复向量空间范畴伴随关系的具体模型，用隐藏的遗忘函子解释叠加类型 S。
2023-10-11 cs.LO math.LO
Lambda Calculus Synopsis
本文给出了一个粗略的，但线性的总结，涵盖了一些关键的定义，符号，和命题从λ演算：它的语法和语义，经典专着由巴伦德雷。首先，我们定义了一个无类型可拓λ演算理论。然后，一些句法糖，一个系统的组合逻辑，和不动点定理进行了描述。最后一节介绍了一个拓扑上的一套lambda条款，这是为了解释一个虚幻的矛盾。也就是说，定义在lambda项集合上的函数在lambda项集合本身中，后者是可数集合。然而，在lambda项的集合上的函数看起来相对于树的拓扑是连续的。
2013-10-24 cs.LO math.GN math.LO
Gentzen-Mints-Zucker duality
Curry-Howard对应通常被描述为将证明（在直觉自然演绎中）与程序（在简单类型lambda演算中的术语）相关联。然而，这种叙述并不是完美的，因为割消的计算内容和lambda演算的逻辑起源。我们重新审视霍华德的工作，并解释它作为一个同构的一类证明在直观的λ演算和一类简单类型的lambda演算的条款。在我们讲述这个故事时，基本的二重性不是证明和程序之间的二重性，而是在一个共同的逻辑计算数学结构上的局部（λ演算）和全局（λ演算或自然演绎）观点之间的二重性。
2020-08-23 cs.LO math.LO
Graphic lambda calculus
我们介绍和研究图形λ演算，一个可视化的语言，可用于表示无类型的λ演算，但它也可以用于紧急代数的计算或表示局部平面缠结图的Reidemeister移动。
2013-09-24 cs.LO math.GT math.LO
An Introduction to the Clocked Lambda Calculus
我们简要介绍了时钟λ演算，一个扩展的经典λ演算与一元符号τ用于见证β步骤。与经典的λ演算相比，这种推广是无穷强正规化的和无穷汇合的。无限范式是丰富的Boehm树，我们称之为钟控Boehm树。
2014-05-29 cs.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
$λ$-Scale, a lambda calculus for spaces with dilations
$λ$ -Scale是λ演算的一个扩充，它适用于突现代数。因此，它可以用于具有伸缩的度量空间。
2012-05-23 cs.LO math.LO math.MG
Lecture notes on the lambda calculus
这是一组课堂讲稿，是我2001年在渥太华大学，2007年和2013年在达尔豪西大学教授的λ演算课程的基础上发展起来的。这些笔记涵盖的主题包括无类型λ演算、Church-Rosser定理、组合代数、简单类型λ演算、Curry-Howard同构、弱规范化和强规范化、多态性、类型推断、指称语义、完全偏序和PCF语言。
2013-12-26 cs.LO
Feasible reactivity in a synchronous pi-calculus
反应性是同步程序的一个基本属性。非正式地说，它保证了在每一个时刻，输入的程序将“反应”产生一个输出。在目前的工作中，我们考虑一个完善的财产，我们称之为“可行的反应性”。除了反应性之外，这个属性保证了在每个时刻，程序的大小和反应时间都受到计算开始时参数大小和最大输入大小的多项式的限制。我们提出了一种方法来注释程序，我们开发了相关的静态分析技术，保证可行的反应程序中表示的S-π演算。后者是基于SL同步编程模型的pi演算的同步版本。
2007-02-11 cs.LO
A Categorical Model for the Lambda Calculus with Constructors
带构造函数的λ演算是带变元构造函数的λ演算的扩展。它将ML模式匹配分解为对常量的实例分析和实例与应用构造之间的交换规则。虽然这种交换规则与通常的计算直觉不匹配，但它使微积分具有表达性和融合性，语法相当简单。本文对带构造函数的λ演算定义了一个合理的范畴模型概念。然后，我们证明了这个定义是完整的片段的演算没有匹配失败，使用模型的部分等价关系。
2012-03-05 cs.LO
Effective lambda-models vs recursively enumerable lambda-theories
一个长期存在的公开问题是，是否存在一个非语法模型的无类型的代数演算，其理论正是最小代数理论（l-beta）。在本文中，我们研究了一个更一般的问题，即（非类型化）代数演算模型的方程/序理论是否可以递归地可递归（r.e.）。为了简洁起见）。我们引入了一个概念的有效模型的Alzuda演算演算，其中包括特别是所有的模型单独介绍的文献。我们证明了有效模型的序理论是不成立的;由此可见，它的方程理论不可能是l-β或l-β-η。然后，我们表明，没有有效的模型生活在稳定或强稳定的语义有一个r.e.等式理论在Scott语义的基础上，我们研究了图模型类，证明了图模型的序理论是不成立的，在所有的图模型理论中，存在一个有效的图模型，它的方程/序理论是最小的。最后，我们证明了这类图模型具有一种向下的Lowenheim-Skolem定理。
2008-06-13 cs.LO math.LO
Determinacy in a synchronous pi-calculus
S-pi-演算是基于SL模型的同步pi-演算。后者是Esterel模型的放松，其中对一瞬间内没有信号的反应只能发生在下一瞬间。在目前的工作中，我们提出并证明了一个组合语义的S-pi演算标记的过渡系统和互模拟的基础上适当的概念。基于这个语义框架，我们探讨了确定性的概念和相关的（局部）汇合。
2008-02-11 cs.LO
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
Semantics of Typed Lambda-Calculus with Constructors
我们提出了一个Curry风格的二阶类型系统，具有并集和交集类型的Arbiser，Miquel和Rios的构造器的λ演算，扩展的λ演算与可变构造器的模式匹配机制。然后，我们证明了强规范化和匹配失败的限制，这个系统的情况下，通过适应标准的reductionmethod。
2011-03-16 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
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
The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi
λ演算中对绑定的内在处理使其成为一种理想的数据结构，用于表示具有绑定的语法对象，如公式、证明、类型和程序。在实现中支持这样的数据结构由于相对于λ项的替换操作的复杂性而变得困难。在本文中，我们提出了悬浮演算，明确处理Meta级绑定的λ演算。我们证明这个演算的性质，使它成为一个合适的替代λ演算的实施。最后，我们比较了悬浮演算与其他显式处理的替代。
2007-02-05 cs.LO cs.PL
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
Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics
我们证明了模型检验问题对于认知μ演算的一个片段是可判定的。该片段允许自由变量的范围内的认知模态的限制形式，避免构建公式体现任何形式的共同知识。我们的演算包含已知的可判定的片段的认识CTL/LTL。它的模态变体可以表示两人博弈中的获胜策略，其中一个玩家具有不完美信息和不可观察的目标，并且，通过适当的编码，具有不完美信息和完美召回的ATL的模型检验问题的可判定实例可以编码为这种认知μ-演算的模型检验问题的实例。
2012-07-14 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
ASMs and Operational Algorithmic Completeness of Lambda Calculus
我们表明，λ演算是一个计算模型，它可以逐步模拟任何顺序确定性算法的任何可计算函数的整数或字或任何数据类型。更正式地说，给定一个算法以上的一个家庭的可计算的功能（作为原始工具，即，算法的一种预言函数），对于每个足够大的常数K，该算法的每个计算步骤可以通过在具有上述考虑的函数族中的常数的λ演算的自然扩展中的恰好K个连续约简来模拟。证明是基于一个不动点技术在λ演算和古列维奇顺序论文，它允许识别顺序确定性算法与抽象状态机。这扩展到部分可计算函数的算法，以这种方式，以异常结束的有限计算与有限约简相关联，从而导致具有特定非常简单特征的项。
2010-10-13 cs.CC cs.LO math.LO
A Braided Lambda Calculus
本文提出了一种带辫子的无类型线性λ演算，相应的组合逻辑，以及交叉G-集给出的语义模型。
2021-12-30 cs.LO cs.PL
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
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
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
On the Validity of Encodings of the Synchronous in the Asynchronous $π$-calculus
进程演算可以通过它们之间的编码来比较它们的表达能力。Gorla提出了一个被广泛接受的定义，定义了什么构成了一个有效的编码，用于证明过程演算之间的相对表达性结果。在这项工作之前，不同的编码和分离结果通常是使用不同的，往往是不兼容的，编码的质量标准。有效编码的教科书例子是Boudol和Honda & Tokoro提出的将同步无选择$π$ -演算编码到其异步片段中的编码，说明后者的表达能力不亚于前者。在这里，我正式确定这些编码确实满足Gorla的标准。
2018-04-26 cs.LO
A synchronous pi-calculus
SL同步编程模型是Esterel同步模型的松弛，其中对瞬时内没有信号的反应只能在下一瞬时发生。在以前的工作中，我们已经重新审视了SL同步编程模型。特别是，我们讨论了一种替代设计的模型，包括线程产卵和递归定义，介绍了CPS翻译的尾部递归形式，并提出了互模拟等价的概念。在目前的工作中，我们扩展了尾递归模型与一阶数据类型获得一个非确定性同步模型的复杂性是一个的pi演算。我们表明，我们的互模拟等价的方法可以应付这种扩展，特别是标记的互模拟可以表征为上下文互模拟。
2007-02-09 cs.LO cs.PL
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
Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Long Version)
本文研究了对普洛特金的按值调用λ-演算的扩展--洗牌演算的执行时间（即，如果有的话，导致范式的β_v-步数）进行语义解释的可能性.为此，我们使用一个线性逻辑为基础的指称模型，可以被看作是一个非幂等的交集类型系统：关系语义。我们的研究受到线性逻辑证明网和无类型按名称调用λ演算的类似研究的启发。我们首先证明了一个定性的结果：一个（可能是开放的）长期是规范化的弱减少（不减少抽象），当且仅当其解释是不空的。然后，我们表明，类型派生的大小可以用来衡量执行时间。最后，我们表明，不同于线性逻辑和按名称调用λ演算的情况，包含在类型推导中的定量信息不会提升到类型（即术语的解释）。为了在按值调用设置中获得执行时间的真正语义度量，我们推测需要对其语法和操作语义进行细化。
2018-12-27 cs.LO math.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
