The Name-Passing Calculus
名字传递演算是移动计算的基础模型。对这些模型的研究已经产生了丰富的结果，从相对表达到编程语用学。这些结果的多样性要求澄清和重组。本文采用与模型无关的方法对传名结石进行了研究，使之得到统一的处理和简化。本文提出的技术工具和结果构成了命名传递演算理论的基础。
2015-08-01 cs.LO
Encodability and Separation for a Reflective Higher-Order Calculus
Meredith和Radestock的$ρ$ -calculus（反射高阶微积分）是一种类似于$π$ -calculus的语言，具有一些不寻常的特性，特别是结构化名称，自由名称的运行时生成，以及缺乏用于名称的范围可见性的运算符。这些功能提出了一些有趣的困难证明的可编码性和分离的结果。我们描述了两个错误，在以前发表的尝试编码的$π$-演算的$ρ$-演算的梅雷迪思和Radestock。然后，我们给出了一个新的编码，并证明其正确性，使用一组编码标准接近Gorla提出的，并讨论了必要的适应工作与演算与运行时生成的结构化名称。最后我们证明了一个分离结果，证明了$ρ$ -演算不能编码在$π$ -演算中.
2022-09-06 cs.LO
Name-free combinators for concurrency
Yoshida演示了如何在异步pi演算中消除来自输入前缀的绑定名称，但她的组合子仍然依赖于“new”运算符来绑定名称。我们修改吉田的组合子替换为“新”和复制反射运营商提供第一个组合子演算没有绑定的名称到异步π演算有一个忠实的嵌入。我们还表明，多分类的Lawvere理论丰富的图形足以捕捉的演算的操作语义。
2019-04-19 cs.LO
A Proof System with Names for Modal Mu-calculus
不动点是语义学、抽象解释和程序逻辑中的一个重要组成部分。它们添加到逻辑中可以增加相当大的表达能力。一个普遍的问题是如何定义这种逻辑的证明系统。在这里，我们将研究模态逻辑与不动点的证明系统。我们提出了一个Tableau证明系统，用于检查公式的有效性，它使用名称来跟踪不动点变量的展开，如Jungteerapanich所设计的。
2013-09-20 cs.LO
Representing operational semantics with enriched Lawvere theories
许多术语演算，如λ演算或pi演算，涉及名称的绑定器，并且绑定变量名称的数学是微妙的。Schoenfinkel在1924年引入了SKI组合子演算，通过消除量化变量来澄清它们在直觉逻辑中的作用。Yoshida演示了如何在异步pi演算中消除来自输入前缀的绑定名称，但她的组合子仍然依赖于new运算符来绑定名称。最近，Meredith和Stay展示了如何修改Yoshida的组合子，用反射算子替换new和replication，以提供第一个没有绑定名称的组合子演算，异步pi演算可以忠实地嵌入其中。在这里，我们提供了一组替代的组合子，它由SKI加上反射构建，也消除了所有的标称现象，但提供了一个忠实的嵌入反射高阶π演算。我们表明，有效地消除了语法糖的名义功能，多分类的Lawvere理论丰富的图形足以捕捉的操作语义的演算。
2017-04-10 cs.LO
Using Session Types for Reasoning About Boundedness in the Pi-Calculus
深度有界和名称有界过程的类是π演算的片段，其中一些对于完整演算不可判定的决策问题变得可判定。P是深度有界的，如果每一个减少序列P包含后继进程与最多k个积极的嵌套限制。P是k级名有界的，如果P的每个约简序列包含至多k个活动有界名的后继过程。这些进程类的成员是不可判定的。在本文中，我们使用二进制会话类型来决定两个类型系统，给出了一个健全的特性：如果一个进程是良好的类型在我们的第一个系统，它是深度有界的。如果一个进程在我们的第二个更严格的类型系统中是良好类型的，它也将是名称绑定的。
2017-09-04 cs.LO
A simple sequent calculus for nominal logic
名词逻辑是一阶逻辑的变体，它支持抽象语法中的绑定名称的推理。名词逻辑的一个关键特征是新量词，它对新名称（迄今为止未出现在任何值中的名称）进行量化。以前的尝试已经作出了开发方便的规则推理与新的量词，但我们认为，这些尝试都是不完全令人满意的。在这篇文章中，我们开发了一个新的numerical演算的名义逻辑中的规则，新的量词是比以前的尝试简单得多。我们还证明了几个结构和元理论的性质，包括削减消除，一致性，和等价的皮茨公理化的名义逻辑。
2013-12-17 cs.LO
Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines
本文通过将范式互模拟、应用互模拟和上下文等价内化到抽象机中，构造了按名调用和按值调用λ-演算到极简高阶进程演算HOcore的完全抽象编码，并证明该方法可扩展到带控制算子的λμ-演算。
2024-07-02 cs.LO
An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus
Eindhoven University of Technology（埃因霍温理工大学）；University of Bologna（博洛尼亚大学）
本文提出了一种新的beta还原形式，通过分析lambda演算中树的分支，重新定义了beta还原，强调减少过程中的树结构扩展关系。
2026-03-04 cs.LO
Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)
在每一个变式中，因式分解和标准化是两个关键属性，它们显示了结果是如何计算的。我们没有分别证明按名称调用（CbN）和按值调用（CbV）变体的因式分解/规范化，而是只证明一次bang演算（受线性逻辑启发并包含CbN和CbV的扩展），然后我们通过翻译转移结果，获得CbN和CbV的因式分解/规范化。该方法是鲁棒的：它仍然适用于扩展演算与运营商和额外的规则，以模拟一些额外的计算功能。
2021-01-20 cs.LO
First-order store and visibility in name-passing calculi
本文研究π-演算中通过基于可见性的类型系统限制计算仅涉及一阶值存储，并刻画顺序与良括号计算下的行为等价关系。
2025-04-24 cs.LO
Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq
本文展示了几个版本的应用相似性和上下文近似的等价性，因此也应用双相似性和上下文等价性，在LR中，确定性的按需调用λ演算与letrec扩展的数据构造器，情况表达式和Haskell的seq运算符。LR对Haskell核心语言的非类型化版本进行建模。双相似性的使用简化了微积分中的等价性证明，并为程序转换的更方便的正确性证明开辟了一条道路。证明是通过一个完全抽象和满射转换成一个按名称调用的演算，这是一个扩展的阿布拉姆斯基的懒惰λ演算。在后一种演算中，我们的相似性和上下文近似的等价性可以通过豪的方法来证明。相似性基于归纳定义的相似性被传递回LR。从按需调用letrec演算到扩展的按名调用λ演算的转换是两种转换的组合。第一个翻译取代呼叫按需要的策略，按名称的策略和它的正确性是通过利用无穷树展开的letrec表达式出现。第二个翻译编码字母表达式，通过使用多不动点组合子和它的正确性表明语法比较减少两个演算。本文的一个进一步结果是上述演算之间的同构，这也是一个关于字母自由表达式的恒等式。
2015-03-12 cs.LO
Linear-use CPS translations in the Enriched Effect Calculus
丰富的效果演算（EEC）是Moggi的计算元语言的扩展，从线性逻辑中选择原语。本文探讨了丰富的效果演算作为一个目标语言的延续传递式（CPS）的翻译，其中的翻译类型强制延续的线性使用。我们首先观察到，已建立的按值调用和按名称调用线性使用CPS将简单类型的微积分转换为直观线性逻辑（ILL），并在EEC给出的ILL片段中。这两个翻译是统一推广的一个单一的通用翻译的丰富的效果演算本身。作为我们的主要定理，我们证明了EEC的通有自翻译是对合的同构。作为推论，我们得到完整的完整性结果，无论是通用的翻译，并为原来的调用按值和按名称的翻译。
2012-10-04 cs.LO
The Functional Machine Calculus III: Choice (Early Announcement)
本文扩展函数机器演算以支持异常处理与循环构造，在保持合流归约和类型化终止性的前提下，增强其表达计算效应的能力。
2024-11-07 cs.LO
On the Computation Power of Name Parameterization in Higher-order Processes
参数化扩展了高阶过程的抽象能力（类似于微积分中的抽象能力），并且被认为能够增强表达能力。本文重点介绍了参数化的名称，即一个结构，映射一个名称到一个进程，在高阶设置。我们提供了两个结果，其计算能力。首先，名称参数化带来了一个完整的模型，在这个意义上，它可以表达一个基本的交互式模型与内置的递归函数。其次，我们比较了名称参数化与著名的π演算，并提供了两个编码之间。
2015-08-20 cs.LO
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
我们研究的编程结构的互动“新”，它产生静态范围的名称，通过信道上的消息通信。这种交互在安全协议中至关重要，这是我们工作的主要激励示例，它也出现在其他编程语言上下文中。我们定义了应用π演算，一个简单的，一般的π演算的扩展，其中的值可以形成从名称通过应用程序的内置函数，受方程，并作为消息发送。(In相比之下，纯pi演算缺少内置函数，它的唯一消息是原子名。我们开发的语义和证明技术，这种扩展的语言，并将其应用于推理安全协议。本文基本上包含了2001年介绍应用π演算的会议论文。它填补了空白，结合改进，并进一步解释和研究应用π演算。自2001年以来，应用π演算一直是许多进一步工作的基础，在许多研究出版物中描述，有时体现在有用的软件中，例如ProVerif工具，它依赖于应用π演算来支持安全协议的规范和自动分析。虽然本文的目的不是要成为一个完整的审查的主题，它受益于进一步的工作，并提供了更好的基础，其中一些。特别是，应用π演算已经通过其在ProVerif的实现演变，目前的定义反映了这种演变。
2017-07-28 cs.CR cs.LO
The Cpi-calculus: a Model for Confidential Name Passing
在分布式系统中共享机密信息在许多应用中是必要的，然而，它打开了控制信息共享的问题，即使在可信方之间。在本文中，我们提出了一个正式的模型，在该模型中，信息的传播是禁用在语法级别的直接方式。我们介绍了一个子演算的π演算，其中通道被认为是机密信息。相对于π演算的唯一区别是，一旦收到的通道不能转发later on. By的例子，我们给出了一个初步的想法，如何在过去已经研究过的一些隐私概念，如组创建和名称隐藏，可以表示没有任何额外的语言结构。我们还提出了一个编码的（无和）π演算在我们的演算。
2019-09-12 cs.LO cs.PL
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
Proof-relevant pi-calculus
形式化π演算是对逻辑框架和机械化元理论系统的表达能力的启发性测试，因为存在名称绑定、带有名称挤出的标记转换、互模拟和结构一致性。形式化已经在各种系统中进行，主要集中在充分研究（和具有挑战性）的属性，如过程互模拟理论。我们提出了一个形式化的Agda，而不是探讨理论的并发转换，残留，因果等价的痕迹，这是以前没有正式的π演算。我们的形式化采用德Bruijn指数和依赖类型的语法，并对齐的“证明转换”提出的Boudol和Castellani在CCS的上下文中与自然存在的Agda的表示标记的过渡关系的证明条款。我们的主要贡献是证明了“钻石引理”的剩余的并发过渡和一个正式的定义等价的轨迹置换的过渡。
2015-07-29 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
(Towards a) Statistical Probabilistic Lazy Lambda Calculus
本文研究了统计概率编程语言模型的需求，提出通过结合开放互模拟和概率模拟等传统工具即可满足这些需求。
2024-03-22 cs.LO
Lambda Calculus with Explicit Read-back
本文介绍了一种新的长期重写系统，这是类似于嵌入式读回机制的互动网络在我们以前的工作，但更容易遵循比在原来的设置，从而分析其属性。也就是说，我们验证了它正确地代表了λ演算。此外，我们表明，有一个减少序列，在我们的长期重写系统中的任何一项开始。最后，我们代表了最左边的策略，这是已知的正常化。
2018-08-20 cs.LO
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
本文将对偶演算推广为归纳型和余归纳型。本文首先介绍了一个非确定性的对偶演算的归纳和共归纳类型。它除了具有原对偶演算的对偶性外，还具有归纳型和余归纳型的对偶性，即归纳型和余归纳型的项和余项的对偶性及其归约规则的对偶性。它的强正规化也被证明，这是通过将其转化为一个二阶对偶演算。通过将二阶对偶演算转化为二阶对称λ演算，证明了二阶对偶演算的强正规化。本文接着介绍了归纳型和共归纳型对偶演算的按值调用系统和按名调用系统，并说明了按值调用和按名调用的对偶性、Church-Rosser性质和强规范性。通过将它们转化为具有归纳和共归纳类型的非确定性对偶演算，证明了它们的强规范化性。
2013-03-27 cs.LO cs.PL
Mirroring Call-by-Need, or Values Acting Silly
Inria & LIX, Ecole Polytechnique（法国国家信息与自动化研究所与巴黎综合理工学院LIX实验室）；Université Paris Cité, CNRS, IRIF（巴黎西岱大学、法国国家科学研究中心与IRIF实验室）
设计一个对称于按需调用的退化演算（按傻调用），通过重写性质和多类型验证其设计，证明按傻调用与按值调用在上下文等价上一致，揭示按值调用上下文等价对效率的盲目性。
2026-06-17 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
Using Pi-Calculus Names as Locks
本文引入类型系统将异步pi-calculus名字用作锁，支持锁释放，保证无死锁和无泄漏，并研究类型化行为等价。
2023-09-13 cs.LO cs.PL
Lambda Calculus and Probabilistic Computation
我们介绍了两个扩展的$λ$演算的概率选择操作，$Λ_\oplus^{cbv}$和$Λ_\oplus^{cbn}$，分别按值调用和按名称调用概率计算。我们证明，都享有合流和标准化，在一个扩展的方式：我们重新审视这两个基本概念，考虑到渐近行为的条款。这两种演算的共同根源是基于线性逻辑的进一步演算，$Λ_\oplus^!$，它允许对选择和复制之间的交互进行精细控制，并允许我们开发统一的模块化方法。
2019-05-10 cs.LO
Light Logics and the Call-by-Value Lambda Calculus
所谓的轻逻辑已经被引入作为具有相当显著的规范化性质的逻辑系统。然而，从这些逻辑为纯λ演算设计类型分配系统是有问题的。在本文中，我们表明，从通常的按名称调用的转换到按值调用的λ演算允许恢复与底层逻辑的强连接。这将在基本仿射逻辑（EAL）的上下文中完成，设计一个自然演绎风格的类型系统，将EAL公式分配给lambda项。
2008-11-07 cs.LO
Proof-Relevant Logical Relations for Name Generation
本文提出用证明相关逻辑关系为带递归的名称生成语言构建直接风格模型，解决动态分配单子构造失效问题，并提供一个易于理解的介绍性场景。
2018-03-29 cs.LO
A type system for Continuation Calculus
由Geron和Geuvers提出的连续演算（CC）是函数计算的一个简单的基础模型。它与λ演算和项重写密切相关，但它没有变量绑定，也没有模式匹配。它是图灵完备的，求值是确定性的。通过选择适当的函数定义，可以使用“按值调用”和“按名称调用”计算这样的概念：例如，有一个按值调用和一个按名称调用的加法函数。在本文中，我们使用类型扩展CC，以便能够以规范的方式定义数据类型，并通过迭代定义这些数据类型的函数。数据类型定义遵循所谓的数据“Scott编码”，而不是更熟悉的“Church编码”。迭代方案有两种：按值调用和按名称调用迭代方案。按值调用变体是按名称调用迭代的双重否定变体。双重否定转换允许在按名称调用和按值调用之间移动。
2014-09-11 cs.LO cs.PL
Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness
这项工作提出了易于处理的双向模拟高阶π演算会话原语（HOPI），并提供了一个完整的研究其最重要的子演算的表达能力。首先，我们开发了三种类型的互模拟，这是符合上下文对等。这些特征表明，仅观察高阶值的特定有限集合（其存在于会话类型中）作为输入就足以推理HOp过程。接下来，我们确定HO，一个最小的，二阶的HOPI子演算，其中高阶的应用程序/抽象，名称传递和递归是缺席的。我们表明，HO可以编码HOPI扩展高阶应用程序和抽象，一阶会话π演算可以编码HOPI。这两种编码都是完全抽象的。我们还证明了会话π演算与共享名称的传递不能被编码到HOPI没有共享名称。我们表明，HOPI，HO和PI是同样的表达; HO的表达能力，使有效的推理类型等价的高阶过程。
2015-02-10 cs.LO
On the Expressiveness of Joining
通信原语的表达性已经在一个基于π演算的公共框架中进行了探索，考虑了四个特征：同步性（异步与同步），arity（一元与多元数据），通信介质（共享数据空间与基于通道）和模式匹配（绑定到名称与测试名称相等性与意图性）。这里考虑另一个维度协调，它说明发生交互所需的过程数量。协调将二进制语言（如pi演算）推广到结合输入的连接语言（如Join Calculus和一般会合演算）。本文通过可能性/不可能性的编码，说明了协调性与其他特征无关。也就是说，连接语言比二进制语言更具表达力，并且没有其他特征的组合可以将连接语言编码为二进制语言。此外，接合不能编码任何其他特征，除非它们可以以其他方式编码。
2015-08-20 cs.LO
On the Simply-Typed Functional Machine Calculus: Categorical Semantics and Strong Normalisation
本文研究函数机器演算（FMC）的范畴语义与强正规化，证明其在适当等式理论下对应自由笛卡尔闭范畴，并扩展 Gandy 证明以确立带类型 FMC 项的强正规化性质。
2023-05-25 cs.LO
Higher-order Processes with Parameterization over Names and Processes
参数化扩展了高阶过程的抽象和应用能力（就像在微积分中的那些）。这个扩展是严格的，即，配备有参数化的高阶过程在计算上更强大。本文研究了高阶过程的两种参数化：一种是关于名称的参数化，另一种是关于过程本身的参数化。我们提出了两个结果。一个是，在参数化的存在下，高阶过程可以以一种非常整洁的方式编码一阶（名称传递）过程，与没有参数化的高阶过程根本不能编码一阶过程的事实相反。在另一个结果中，我们提供了一个更简单的表征（标准）上下文互模拟高阶过程的参数化，在正常的互模拟，源于众所周知的正常表征高阶微积分。这两个结果表明，更本质的参数化方法在高阶范式的表达性和行为等效。
2016-08-10 cs.LO
Approximation theory for distant Bang calculus
Université de Lorraine（洛林大学）；CNRS（法国国家科学研究中心）；Inria（洛林信息与自动研究实验室）；LORIA（奥尔良大学）；Université d’Orléans（中央理工-卢瓦尔河学院）；INSA CVL（信息科学与计算实验室）；LIFO（巴黎东克雷泰伊大学）；Université Paris Est Creteil（应用与理论语言学实验室）；LACL
本文研究远距离Bang演算的近似语义，定义了Böhm树和泰勒展开，并将其推广到Call-by-Name和Call-by-Value中，提供统一的无限和资源敏感语义框架。
2026-07-01 cs.LO
A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on
我们介绍了一个范畴理论抽象的语法与辅助功能，称为admissiblemonad态射。依赖于结构递归的抽象形式，我们设计了通用工具，从基本数据中构造容许单子态射。这些工具自动化了普遍存在的标准模式，如（1）在连续的、潜在依赖的层中定义辅助函数，以及（2）通过语法归纳来证明辅助函数的属性。我们涵盖了文献中的重要例子，包括标准的捕获避免替换的Aluda-calculus，具有bindingevaluation上下文的Aluda-calculus，具有命名替换的Aluda-mu-calculus，以及微分Aluda-calculus。
2022-04-08 cs.LO cs.PL math.CT
Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution
我们提出了一个完整的形式化的标准化定理的Martin-Löf的构造类型论的λ演算使用一阶语法与一种名称的自由和绑定变量和斯托顿的多重替代。我们的形式化是基于Ryo Kashima的证明，其中具有标准序列的beta-约简的概念被归纳关系捕获。证明只使用结构归纳法的语法和定义的关系，这是可能的，由于我们采用的特定公式的替代。整个开发过程使用Agda系统进行了机器检查。
2018-07-05 cs.LO
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
Continuation calculus
带有控制的程序通常使用扩展了控制算子的λ演算建模。我们不修改λ演算，而是考虑一种不同的计算模型。我们介绍连续演算，或CC，确定性的计算模型，仅使用头减少评估，并认为它是适合的建模程序与控制。它演示了如何定义程序，指定它们，并证明它们是正确的。这是通过在CC中呈现一个列表乘法程序来详细展示的，该程序在遇到零时过早返回。正确性证明包括程序的终止。在连续演算中，我们可以对按名称调用和按值调用进行建模。此外，按名称调用函数可以应用于按值调用结果，反之亦然。
2013-09-05 cs.LO cs.PL
Decomposing Probabilistic Lambda-calculi
概率演算的概念通常带有一个规定的归约策略，通常是按名称调用或按值调用，因为演算是非融合的，这些策略会产生不同的结果。这是一个突破的主要优势之一，微积分：融合，这意味着结果是独立于战略的选择。我们提出了一个概率的概率运算符分解成两个语法结构：一个发电机，它代表一个概率事件;和消费者，它的行为取决于一个给定的事件的条款。由此产生的演算，概率事件Lambda演算，是融合的，并解释调用的名称和调用的值策略，通过不同的解释概率运算符到我们的生成器和消费者结构。我们提出了两个概念的减少，一个通过细粒度的本地重写步骤，和一个通过生成和消费的概率事件。演算的简单类型基本上是标准的，它们传达了强规范化。我们演示了如何编码按名称调用和按值调用的概率评估。
2020-02-19 cs.LO cs.PL
What is a categorical model of the differential and the resource lambda-calculi?
本文给出了无类型微分代数演算和资源演算的抽象模型理论。特别地，我们提出了这些演算模型的一般定义，即笛卡尔闭微分范畴中的线性自反对象的概念。提供了基于关系的模型的例子。
2010-11-10 cs.LO
The Bang Calculus and the Two Girard's Translations
我们研究了两个吉拉德的翻译到线性逻辑的直觉蕴涵利用Bang演算，一个范式的功能语言与一个明确的框运算符，允许调用的名称和调用的值ALGODA演算编码。我们调查如何从句法和语义的角度来看，爆炸演算包括调用的名称和调用的值的类演算。
2019-04-15 cs.DM cs.LO cs.PL
Calculi for Intuitionistic Normal Modal Logic
本文给出了一个按名称调用和一个按值调用的项演算，它们都与直觉模态逻辑IK的盒片段有Curry-Howard对应关系。显示了结石的强归一化性和汇合性。此外，我们还定义了一个从按值调用演算到按名称调用演算的CPS转换，并证明了它的可靠性和完备性。
2016-06-10 cs.LO cs.PL
Probabilistic Programming Semantics for Name Generation
我们做一个正式的类比之间的随机抽样和新鲜的名字生成。我们表明，准Borel空间，概率规划模型，可以合理地解释斯塔克的$ν$ -演算，演算的名称生成。此外，我们证明了这种语义是完全抽象的一阶类型。这是令人惊讶的“现成的”模型，并需要一个新的分析函数空间上的概率分布。我们的工具是多样的，包括描述集理论和范式的$ν$ -演算。
2020-12-20 cs.LO cs.PL math.LO
Pure Pattern Calculus à la de Bruijn
在程序设计语言领域中众所周知的是，处理变量名和绑定器可能导致冲突，诸如在实现解释器或编译器时的不期望的捕获。这种情况已经通过求助于de Bruijn索引来克服，其中绑定器仅捕获一个变量名，如$λ$ -演算。这种方法的优点在于，当使用索引时，所谓的$α$ -等价变成了语法上的相等。近年来，模式演算由于其表现力而获得了相当大的关注。他们原来是出了名的方便，研究现代函数式程序设计语言的基础建模功能，如模式匹配，路径多态性，模式多态性等，但是，文献不足，当涉及到处理$α$转换和绑定器同时捕获几个变量名。纯模式演算（PPC）就是这种情况：它是$λ$的自然扩展--允许抽象几乎任何术语的演算。本文扩展了de Bruijn的思想，以适当地克服多绑定问题，通过引入一种新的表示PPC的二维索引，在努力实现一个原型的类型化函数式程序设计语言的基础上PPC，捕获路径多态性。
2020-06-28 cs.LO cs.PL
A program logic for fresh name generation
我们给出了Pitts和Stark的ν-演算的程序逻辑，它是按值调用的简单类型λ-演算的扩展，具有生成新名称的机制。可以比较名字是否相等，从而产生具有细微可观察属性的程序。由生成和抽象之间的交互产生的隐藏名称通过类型上下文上的二阶量词逻辑地捕获。我们说明使用的逻辑推理著名的困难的情况下，从文献。
2021-03-12 cs.LO cs.PL
List types for resource aware languages: an implicit name approach
University of Novi Sad, Faculty of Technical Sciences（新萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；University of Lyon, École normale supérieure de Lyon（里昂大学里昂高等师范学院）
本文提出了一种基于隐式名称的列表类型方法，用于在资源感知语言中实现线性性，并通过Haskell实现了相关语言和计算模型。
2026-01-13 cs.LO math.LO
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
我们研究了一类简单类型的λ演算的名义代数Henkin式模型，其中变量映射到表示中的名称，而λ演算抽象映射到（非功能性的）名称抽象操作。由此产生的表示更小，更好的行为，在我们精确的方式，比基于函数值的模型。使用这些新的模型，我们然后开发了一个概括的λ-长期语法丰富他们的存在元变量，从而产生一个理论的不完整的功能。这种不完备性与函数抽象和应用给出的不完备性的通常概念是正交的，并且对应于洞和不完备对象。
2011-11-01 cs.LO cs.PL
Formalizing $φ$-calculus: a purely object-oriented calculus of decorated objects
存在许多演算用于对面向对象语言的各种特性进行建模。它们中的许多都是基于$λ$ -演算的，并且专注于基于静态类型的类语言或基于动态原型的语言。我们正式的装饰对象，非正式地提出了Bugayenko，这是定义在对象和依赖于装饰作为一个主要的机制对象扩展的无类型演算。它不是基于$λ$ -演算，但只有四个基本的语法结构是一样完整的。我们证明了演算是合流的（即具有Church-Rosser性质），并介绍了一个抽象的机器调用的名称评估。最后，我们提供了一个健全的翻译$λ$ -演算记录。
2022-12-02 cs.LO cs.PL
Topological Self-Stabilization with Name-Passing Process Calculi
拓扑自稳定描述了分布式系统让节点自己建立有意义的覆盖网络的能力。独立于初始网络拓扑，系统通过转发、插入和删除到相邻节点的链路收敛到期望的拓扑。名字传递进程演算，如pi演算，是一种众所周知的和广泛使用的方法来建模并发和分布式算法。π演算被设计为自然地表达具有变化的链接基础设施的进程，因为进程之间的通信可以携带可以用于进程之间的链接的变化的信息。我们重新设计了一个简单的本地线性化算法，异步消息传递，最初是为共享内存模型设计的。我们使用一个扩展的本地化的π演算，一个变种的π演算，模型的算法。随后，我们正式证明了自稳定性的封闭性，弱收敛性的任何初始配置，和强收敛性的两个特殊情况。在我们的证明中，我们使用的是断言推理而不是基于行动的风格。此外，我们描述了在一般情况下证明（强）收敛的挑战。此外，我们给出了强收敛的强有力的论据，支持进一步证明引理，并讨论了不同的方法进行正式证明。
2016-04-14 cs.DC cs.LO
Graph rewrites, from graphic lambda calculus, to chemlambda, to directed interaction combinators
在这里，我报告的修改和图形λ演算之间的关系，各种形式主义下出现的名称chemlambda和一个版本的定向交互组合。这是人工化学chemlambda研究和实验的一部分，以及与λ演算或相互作用组合子的关系，如arXiv：2003.14332中所述，可从https://chemlambda.github.io/index.html的入口页面获取
2020-07-07 cs.LO math.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
Putting a Spin on Language: A Quantum Interpretation of Unary Connectives for Linguistic Applications
Institute for Theoretical Physics（理论物理研究所）；Center for Complex Systems Studies（复杂系统研究中心）；Utrecht University（乌得勒支大学）；Utrecht Institute of Linguistics OTS（乌得勒支语言学研究所OTS）
目前在计算语言学中使用的Lambek演算的扩展版本依赖于一元模态，以允许影响词序和短语结构的结构规则的受控应用。这些受控的结构操作引起的衍生歧义，错过了原来的Lambek演算或其pregroup简化。已经提出了在FVect和线性映射的紧凑闭范畴中对扩展的Lambek演算进行组合解释的建议，但是在这些建议中，语法语义映射忽略了控制模态，有效地将它们的作用限制在语法中。我们的目标是把模态变成向量解释的一等公民。在方向密度矩阵语义的基础上，我们用一个额外的自旋密度矩阵空间扩展了类型系统的解释。证明的解释，然后在模糊的推导结果与正交自旋状态张紧。我们的方法引入了一种同时表示歧义话语的共存解释的方式，并为词汇和派生歧义的整合提供了一个统一的框架。
2021-09-06 cs.CL cs.LO quant-ph
The Buffered π-Calculus: A Model for Concurrent Languages
基于消息传递的并发语言广泛应用于大型分布式系统和协同系统的开发。本文介绍了缓冲$π$演算-一个变种的$π$演算的通道名称分为缓冲和无缓冲：通信沿缓冲通道是异步的，并保持同步沿无缓冲通道。我们表明，缓冲$π$演算可以完全模拟在polyadic $π$演算强互模拟。相对于$π$ -演算，这是很难在实践中使用，新的语言，使简单和清晰的建模的实际并发语言。我们在缓冲的$π$ -演算中编码了两种现实世界的并发语言：（核心）Go语言和（核心）Erlang。这两种编码是完全抽象的弱互模拟。
2012-12-26 cs.FL cs.LO
