Reactive Turing Machines with Infinite Alphabets
反应图灵机（Reactive Turing machine，RTM）的概念是对具有交互作用的图灵机的正交扩展. RTM用于定义可执行转换系统的概念，就像图灵机用于定义自然数上的可计算函数的概念一样。RTM继承了图灵机所涉及的所有集合的有限性，因此，在单步的中，RTM只能从有限的数据集中传递元素。一些进程演算，如π演算，本质上依赖于无限的动作字母表，因此在这些演算中指定的转换系统是不可执行的。然而，仔细观察，π演算似乎并没有以不可计算的方式使用无限数据。在本文中，我们研究了几种放松有限性要求的方法。我们首先考虑RTM的一个变体，其中所有集合都允许是可数的，我们得到了无限RTM的概念。无限RTMs具有极强的表现力，因此我们很难将其用作表现力标准。然后，我们通过添加额外的限制来改进模型。因此，我们定义了一个原子RTM的概念。它是RTM的一个更受限制的变体，其中动作和数据符号的集合仍然允许是无限的。我们提出了一个名义上的可执行性的概念，基于RTMs与原子，并证明了每一个有效的原子转移系统是名义上可执行的。由此可见，在π演算中可定义的进程在名义上是可执行的。相反，在进程规约语言mCRL 2中，可以指定名义上不可执行的进程。因此，名义上的可执行性为进程演算提供了一个新的表达标准。
2017-02-20 cs.LO
Proof search for propositional abstract separation logics via labelled sequents
分离逻辑是霍尔逻辑的一个扩展族，用于对改变存储器的程序进行推理。这些逻辑是“抽象的”，因为它们独立于任何特定的具体内存模型。他们的断言语言，称为命题抽象分离逻辑，以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。我们发展了一个模块化的证明理论，各种命题抽象分离逻辑使用割自由标记的代数演算。我们首先扩展了Hou等人的BBI的割费标记的代数演算，通过添加部分确定性和可取消性的合理规则来处理Calcagno等人的分离代数的原始逻辑，同时保留割消除。我们通过一个合理的中间演算来证明我们演算的完备性，这个中间演算使我们能够从找不到证明的失败中构建反模型。然后，我们捕获其他命题抽象分离逻辑通过添加健全的规则不可分割的单位和不相交，同时保持完整性。我们提出了一个定理证明的基础上，我们的标记演算这些命题抽象分离逻辑。
2013-11-26 cs.LO
Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality (Extended Abstract)
我们开发了一个有相关模态的Lambek演算的分类成分分布语义，它具有有限版本的压缩和排列规则。语义学的范畴部分是一个monoidal双闭范畴，其上有一个定义在微分范畴上的余代数模态。我们实例化这一类有限维向量空间和线性映射，通过量化函子和工作与三个具体的解释的余代数模态。我们应用该模型来构建分类和具体的语义解释的动机的例子，这个扩展演算：派生的短语与寄生的差距。具体解释的有效性通过消歧任务进行评估，在将句子消歧数据集扩展到寄生间隙短语上，使用BERT，Word2Vec和FastText向量和关系张量
2021-01-26 cs.LO
An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)
Turin University（都灵大学）；Toho University（东海大学）
提出一种带有零、后继和条件算子的无穷Lambda演算，通过全局迹条件确保良类型项的任何无穷归约都强收敛，并证明其与哥德尔系统T等价。
2026-06-24 cs.LO
A Safety and Liveness Theory for Total Reversibility (Extended Abstract)
我们研究了可逆演算中的安全性和活性理论，其中还原是完全有序的，回滚导致系统回到过去的状态。类似于以前的工作通信事务，活性和安全分别对应于应该测试和逆可能测试的前序。我们开发了完全抽象的模型，这些前序在可逆演算，这是只基于向前过渡，从而提供了一个简单的证明技术，完善这样的系统。我们表明，就安全性而言，完全可逆性是CCS的保守扩展。然而，就活性而言，将完全可逆性添加到CCS使更多系统与众不同。据我们所知，这项工作提供了安全性和活性的第一个特征，以及可逆演算的第一个测试理论。
2016-07-29 cs.LO
Implementing the Stochastics Brane Calculus in a Generic Stochastic Abstract Machine
在本文中，我们处理的问题，实现一个抽象的机器随机版本的膜演算。而不是定义一个特设的抽象机，我们认为一般的随机抽象机介绍了拉金，Paulevé和菲利普斯。膜的嵌套结构被扁平化为一组物种，其中层次结构通过名称来表示。为了减少这种编码引入的开销，我们通过添加写时复制优化策略来修改机器。我们证明，这种实现是足够的随机结构操作语义最近给出的膜演算。这些技术也可以移植到其他随机演算处理嵌套结构。
2012-11-17 cs.CE cs.LO
Fully Abstract Game Semantics for Actors
基于参与者的代数理论和异步$π$演算的博弈语义，给出了参与者博弈语义的完全抽象证明。
2019-01-07 cs.LO
Reduction in X does not agree with Intersection and Union Types (Extended abstract)
本文定义了演算X的交集和并集类型赋值，X是一种与经典逻辑的根森演算具有Curry-Howard对应关系的替换自由语言。我们表明，这个概念是封闭的主语扩展，并表明，它需要加以限制，以满足主语减少以及，使其不适合定义的语义。
2011-09-21 cs.LO
String Diagrams for Regular Logic (Extended Abstract)
正则逻辑可以被看作是正则范畴的内部语言，但逻辑本身一般不被给予范畴化的处理。本文用集合T上的自由正则范畴FRG（T）来理解正则逻辑的语法和证明规则。从这个观点来看，正则理论是从一个合适的2-范畴的上下文--FRG（T）中的2-范畴的关系--到偏序集的2-范畴的某些monoidal 2-函子。这样的函子给每个上下文中的公式集赋值，并按蕴涵排序。我们把这样一个2-函子称为一个正则演算，因为它自然地产生了一个图形化的弦图演算的精神Joyal和街。我们将证明，每一个自然范畴都有一个相关联的正则演算，反过来，从每一个正则演算，我们可以构造一个正则范畴。
2020-09-15 cs.LO
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
这项工作利用会话类型的逻辑基础，以确定什么样的类型纪律的π演算可以准确地捕获，并被捕获，π演算的行为。利用证明理论的内容的可靠性和完整性的微积分和自然演绎呈现的线性逻辑，我们开发了第一个相互逆和完全抽象的进程作为函数和函数作为进程编码之间的多态会话π演算和系统F的线性制定。然后，我们能够从会话演算的理论推导出会话演算的结果：（1）我们通过系统F中的代数表示获得归纳和共归纳会话类型的特征;（2）我们将结果扩展到值和进程传递，需要强规范化。
2018-01-25 cs.LO cs.PL
A Higher-order Calculus of Computational Fields
大规模分布式系统的复杂性，特别是当部署在物理空间中时，需要新的机制来解决集体自适应行为的可组合性和可重用性。计算场已经被提出作为有效的抽象来填补这样的系统的宏观级别（指定系统的集体行为）和微观级别（个体设备的计算和交互动作以实现该集体规范）之间的间隙，从而提供基础以更好地促进在更高抽象级别的集体API和复杂系统的工程。本文提出了一个完整的正式基础领域的计算，在一个核心（高阶）演算的计算领域包含一些关键的语法结构，并配备了类型，指称和操作语义。重要的是，这允许正式建立集体自适应系统的微观和宏观层面之间的联系，由（聚合）指称语义相对于（每设备）操作语义的充分抽象和充分性的结果。
2016-10-25 cs.LO
Introduction to Cirquent Calculus and Abstract Resource Semantics
本文介绍了一种改进的微积分的方法，称为cirquent演算。而在Gentzen风格的证明树兄弟姐妹（或堂兄弟姐妹等）序列是不相交的公式序列，在圆微积分中，它们可以共享元素。明确地允许或禁止共享资源，从而将子结构逻辑的资源感知直觉带到一个更微妙的层次，cirquent演算提供了比cirquent演算更大的灵活性和功能。随着可计算性逻辑的诞生，对新的演绎工具的需求也随之而来（见http：//www.cis.upenn.edu/linggiorgi/cl.html）--这是一种语义构建的计算资源形式理论，它顽固地抵制了传统句法方法框架内的任何公理化尝试。循环微积分打破了僵局。从其规则的全部集合中去除收缩，产生了可计算性逻辑的基本片段CL 5的健全和完整的系统。另一方面，在微积分中做同样的事情，会把婴儿和洗澡水一起扔掉，导致严格较弱的仿射逻辑。可计算性逻辑的一个隐含的主张是，它是CL 5，而不是仿射逻辑，充分体现了传统上与后者相关的资源哲学。为了加强这一主张，本文进一步引入了一个抽象的资源语义，并显示了CL 5的可靠性和完整性。
2005-12-23 cs.LO math.LO
Abstraction of Nondeterministic Situation Calculus Action Theories -- Extended Version
Ronin Institute（罗宁研究所）；University of Oxford（牛津大学）；York University（约克大学）
基于非确定性情境演算和ConGolog，提出一个通过细化映射连接抽象与具体动作理论的智能体行为抽象框架，支持策略推理与综合，并证明了抽象层面的强FOND计划可细化为具体层面的有效计划。
2023-05-20 cs.AI cs.LO
Input-based Three-valued Abstraction Refinement
提出基于输入分裂的三值抽象精化（TVAR）算法框架，简化状态空间形式主义，在开源工具machine-check中实现并验证AVR架构机器码系统性质，首次将TVAR实际用于机器码验证且能处理朴素模型检查或CEGAR无法验证的场景。
2025-11-12 cs.LO
Addressing Machines as models of lambda-calculus
本文提出可寻址机器作为λ演算模型，通过仅操作地址的简单机器及最左归约语义，并引入类似ω和ζ_β的规则，构建完整的无类型λ演算模型。
2022-07-28 cs.LO
E-unification for Second-Order Abstract Syntax
本文提出二阶抽象语法的E-合一，融合高阶合一与等式合一思想，实现任意绑定器下的可靠且完备的合一过程。
2023-06-07 cs.LO
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
我们提出了超经典过程（HCP），这是对线性逻辑和π演算之间的“证明作为过程”对应关系的修订解释，最初由Abramsky [1994]提出，后来由Bellin和Scott [1994]，Caires和Pfenning [2010]以及Wadler [2014]等开发。HCP通过保守地将线性逻辑扩展到hyperenuments（环境的集合，受到Avron [1991]的hypersequences的启发），修补了线性逻辑与π演算中并行组合的语法和可观察语义之间的差异。在hyperenvironments的环境分离是内在的$\otimes$，并对应于并行过程的行为。由于这个属性，我们第一次能够从证明重写中提取标记转换系统（lts）语义。利用类型级别上的并行性信息，我们获得了Merro和Sangiorgi [2004]在π演算中为非阻塞I/O建模而制定的延迟操作的逻辑重构。我们定义了一个基于Brzozowski导数的过程的指称语义，并揭示了HCP中的非干扰对应于Fubini的双重反导定理。有一个lts允许我们使用行为理论的标准工具箱来验证HCP。我们对HCP的双相似性和倒刺同余进行了实例化，得到了一个完整的抽象结果：双相似性、指称等价性和倒刺同余一致。
2018-11-06 cs.LO
On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus
本文研究叠加演算中破坏性等式消解对反驳完全性的影响，证明直接加入该操作会导致不完全性，并提出若干保持反驳完全性的受限演算变体。
2024-05-06 cs.LO
Nominalistic Logic (Extended Abstract)
名物化逻辑（NL）是对保罗·吉尔摩的内涵类型论（ITT）的一种新的表述，它是一种逻辑演算和一个简洁的名物化公理（N），在某些情况下，它允许谓词的名称作为个体。该逻辑有一个灵活的理解公理，但没有外延性公理和无穷公理，尽管公理N是导出自然数的皮亚诺公设的关键。
2008-12-28 cs.LO
Positive Sharing and Abstract Machines
针对正向λ演算的自然抽象机存在二次减速的问题，本文提出一种基于与机器环境标准结构对偶的新型切片技术的优化抽象机，并证明其高效性。
2025-09-04 cs.LO cs.PL
A Proof System with Names for Modal Mu-calculus
不动点是语义学、抽象解释和程序逻辑中的一个重要组成部分。它们添加到逻辑中可以增加相当大的表达能力。一个普遍的问题是如何定义这种逻辑的证明系统。在这里，我们将研究模态逻辑与不动点的证明系统。我们提出了一个Tableau证明系统，用于检查公式的有效性，它使用名称来跟踪不动点变量的展开，如Jungteerapanich所设计的。
2013-09-20 cs.LO
Realisability semantics of abstract focussing, formalised
我们提出了一个抽象的焦点，配备了证明条款的微积分：在传统的Zeilberger的工作，逻辑连接词和它们的介绍规则是作为一个参数的系统，它崩溃的同步和异步阶段的焦点作为宏观规则。我们进一步离开作为一个参数的操作，扩展了一个新的假设的背景下，这使我们能够捕捉经典和直观的聚焦微积分。然后，我们定义的可实现性语义（的证明）的系统，蒙奇-Maccagnoni的正交模型的基础上，经典的集中式微积分，但现在在更高的抽象层次上操作上述。在这个层次上，我们证明了一个引理，即如果一个项是A型的，那么在模型中它的外延是在A的（集合论）解释中。这表明了这样一个事实：取集合的正交时所涉及的全称量化在语义中反映了Zeilberger在异步阶段宏观规则中的全称量化。系统及其语义都在Coq中形式化。
2015-11-13 cs.LO
What is a categorical model of the differential and the resource lambda-calculi?
本文给出了无类型微分代数演算和资源演算的抽象模型理论。特别地，我们提出了这些演算模型的一般定义，即笛卡尔闭微分范畴中的线性自反对象的概念。提供了基于关系的模型的例子。
2010-11-10 cs.LO
Extended Abstract: Mutable Objects with Several Implementations
本研究介绍ACL2 8.6版本新增的attach-stobj特性，该特性支持为抽象stobj配置不同可执行操作且无需重新认证相关书籍与定理，同时给出了背景、用户概述及实现说明。
2025-07-25 cs.LO cs.PL
An intensionally fully-abstract sheaf model for $π$ (expanded version)
本文为 $\pi$-演算提出基于简单站点上层的组合模型，该层对应并发无辜策略，并证明其内涵完全抽象于公平测试等价，核心是借助字符串图构造站点。
2017-11-14 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
Reasonable Space for the $λ$-Calculus, Logarithmically
针对$λ$-演算空间代价模型研究不足的问题，本文基于Krivine抽象机变体提出新合理空间代价模型，首次支持对数空间，并研究其时间行为及向传值$λ$-演算的迁移，完善了$λ$-演算的计算代价分析。
2024-11-19 cs.CC cs.LO cs.PL
