Abstract machines for game semantics, revisited
我们定义了新的抽象机器的游戏语义，对应于传统的计算机网络，并可以作为一个中间表示编译目标的分布式系统。这是通过两个步骤实现的。首先，我们介绍了HRAM，一个堆和寄存器抽象机，一个传统的计算机的抽象，它可以被构造成HRAM网，一个抽象的点对点网络模型。HRAM是多线程的，并且通过令牌进行子线程通信（参见或跳跃。游戏抽象机（GAM）是在接口级别具有额外结构的HRAM，但没有特殊的操作能力。我们表明，GAM不能天真地组成，但组成必须使用适当的HRAM组合子介导。HRAM足够灵活，可以表示具有状态（非无辜游戏）或并发（非交替游戏）的语言的游戏模型。我们说明了这种技术的潜力，通过实现一个玩具分布式编译器ICA，高阶程序设计语言与共享状态并发，从而显着扩展我们以前的分布式PCF编译器。我们表明，编译是健全的和内存安全的，即没有（分布式或本地）垃圾回收是必要的。
2013-04-15 cs.LO
A Behavioural Theory of Probabilistic Algorithms Using Probabilistic Abstract State Machines
Software Competence Center Hagenberg（哈根贝格软件能力中心）；Institut Nationale Polytechnique de Toulouse / IRIT CNRS（图卢兹国立理工学院 / 法国国家科学研究中心信息系统研究实验室）
提出概率算法的公理化定义，引入概率抽象状态机（pASM）并证明其能逐步模拟所有满足公理的概率算法。
2026-06-23 cs.LO
Interactive Small-Step Algorithms II: Abstract State Machines and the<br> Characterization Theorem
在早期的工作中，抽象状态机论文-任意算法在行为上等同于抽象状态机-建立了几类算法，包括普通的，交互式的，小步算法。这是在这些类算法的公理化的基础上完成的。在第一部分（交互式小步算法I：公理化）中，公理化被扩展到涵盖不一定是普通的交互式小步算法。这意味着算法（1）可以完成一个步骤，而不必等待对该步骤的所有查询的回复，并且（2）不仅可以使用环境的回复，而且可以使用接收回复的顺序。为了证明论文的算法的这种普遍性，我们在这里扩展的抽象状态机的定义，将明确注意到答复的相对时间和答复的可能性。我们证明了扩展抽象状态机关于第一部分中公理化的一般算法的特征定理。
2007-11-05 cs.LO
B Maude: A formal executable environment for Abstract Machine Notation Descriptions
我们提出了B Maude，一个原型的可执行环境的抽象机器记法实现的Maude语言。B Maude是形式化定义的，它是将AMN的语义实现为$π$框架中的表示的结果，该框架是Mosses的基于一致性的语义和Plotkin的解释自动机的实现。B Maude赋予B方法重写执行、符号搜索和AMN描述的线性时态逻辑模型检验。
2021-08-17 cs.LO cs.SE
The Abstract Machinery of Interaction (Long Version)
本文回顾了Mackie和Danos & Regnier提出的基于Girard交互几何的交互抽象机（Interaction Abstract Machine，IAM）。它是一个不寻常的机器，不依赖于环境，在线性逻辑证明网络上呈现，其可靠性证明是复杂的，并通过各种其他形式主义。在这里，我们提供了一个新的直接证明其正确性的基础上，金沙的改进，一个自然的概念互模拟的变体。此外，我们的证明进行了一个新的介绍IAM，定义为一台机器直接作用于$λ$ -条款，而不是线性逻辑证明网。
2020-07-09 cs.LO cs.PL
TWAM: A Certifying Abstract Machine for Logic Programs
类型保持（或类型化）编译使用类型化派生来证明编译的正确性。我们为Prolog的简单类型方言设计并实现了一个类型保留编译器，我们称之为T-Prolog。我们的方法的关键是一个新的认证抽象机，我们称之为类型沃伦抽象机（TWAM）。TWAM有一个足够强的依赖类型系统来指定逻辑框架LF中的逻辑程序的语义。我们提出了一个合理性元定理，它构成了部分正确性保证：良好类型的程序实现的逻辑程序指定的类型。这个元定理证明了我们的设计和实现的证明编译器从T-Prolog到TWAM。
2018-01-01 cs.LO cs.PL
A Logic for Non-Deterministic Parallel Abstract State Machines
我们开发了一个逻辑，使推理的单步的非确定性并行抽象状态机（ASM）。我们的逻辑建立在统一的逻辑介绍了Nanchen和Stärk推理分层（并行）ASM。我们在这方面的主要贡献是在逻辑形式主义中处理非决定论（有界和无界）。此外，我们这样做，而不牺牲逻辑的完整性的语句的单步的非确定性并行ASM，如规则的不变量，规则的一致性条件，或一步一步的规则等价。
2017-05-30 cs.LO
Positive Sharing and Abstract Machines
针对正向λ演算的自然抽象机存在二次减速的问题，本文提出一种基于与机器环境标准结构对偶的新型切片技术的优化抽象机，并证明其高效性。
2025-09-04 cs.LO cs.PL
A Reversible Crumbling Abstract Machine for Plotkin's Call-by-Value
Alma Mater Studiorum - Università di Bologna（博洛尼亚大学）
本文提出一种可逆碎裂抽象机，用于Plotkin的按值计算，通过控制计算复杂性将β步数转化为成本模型，实现常数空间开销。
2026-05-09 cs.LO
Computing and Proving Well-founded Orderings through Finite Abstractions
检查复杂状态机属性的常用技术是构建一个有限抽象，然后检查抽象系统上的属性--如果抽象被证明是代表性的，则仅将对抽象系统的通过检查转移到原始系统。这种方法确实需要有限抽象的推导或定义，但可以避免复杂的不变量定义的需要。为了检查微处理器中内存事务的进程，我们需要证明复杂状态机中的事务总是进展到完成。作为这项工作的一部分，我们开发了一个过程，用于计算目标状态机的有限抽象图，以及关于抽象图中的弧上的某些度量是否减少的注释。然后，我们迭代地将抽象图分成强连接的组件，然后为抽象图中的每个节点建立一个度量，确保在原始系统的每个过渡中减少，以保证进度。对于有限状态的目标系统（如硬件设计），我们提出了有效地提取抽象图的方法，使用增量SAT通过GL，然后应用我们的过程来检查进展。我们提出了一个实现的面包店算法作为一个例子应用程序。
2020-09-29 cs.LO
A Fully Abstract Model of PCF Based on Extended Addressing Machines
本文证明扩展寻址机（EAMs）对带有显式替换的 PCF 的模拟具有等价性，并基于定义性结果证明通过逻辑关系取商得到的 PCF 模型是全抽象的。
2025-08-05 cs.LO
Crumbling Abstract Machines
用一个共享的构造（如let表达式）扩展了可达演算，使项的特殊表示成为可能：迭代的应用程序通过在它们中的任何两个之间引入共享点来分解，减少到应用程序只有值作为直接子项的情况。这项工作研究如何崩溃的条款表示的影响，设计和抽象的机器按值调用评估的效率。关于设计，它消除了对计算上下文进行编码的数据结构的需要，例如在环境中编码的应用堆栈和转储。关于效率，我们表明，没有减速，特别是澄清肯尼迪提出的一点，关于这种代表性的潜在效率低下。此外，我们证明，一切顺利地扩展到微妙的情况下，开放的条款，需要实施证明助手。在此过程中，我们还指出，延续传递样式转换（可能是我们的表示的替代方案）不会扩展到开放情况。
2019-07-13 cs.LO cs.PL
A Strong Distillery
抽象机器的强评估的非线性项（即，在抽象）是一个最被忽视的话题，尽管他们在实现证明助手和高阶逻辑程序设计语言的使用。本文介绍了一种最简单形式的强求值机，即对范式的最左最外（按名称调用）求值，证明了它的正确性、完备性，并限制了它的开销。这样的机器，被认为是强米尔纳抽象机，是KAM计算范式的变体，只使用一个全局环境。它的性质通过一种特殊形式的解码来研究，称为蒸馏，进入线性替换演算，巧妙地将机器重新制定为显式替换的标准微步策略，即线性最左最外约简，即，线性水头降阶的范式的推广。此外，机器的开销被证明是线性的步骤的数量和初始项的大小，验证其设计。该研究强调了强机器的两个显著特征，即回溯阶段及其与抽象和环境的相互作用。
2016-03-16 cs.LO cs.PL
RNA interference and Register Machines (extended abstract)
RNA干扰（RNAi）是小RNA（siRNA）在没有蛋白质辅助的情况下直接控制基因表达的机制。这种机制由RNA和小RNA之间的相互作用组成，两者都可以是单链或双链的。该机制的靶标是待降解或畸变的mRNA，而引发剂是待切割成siRNA的双链RNA（dsRNA）。观察RNAi的数字性质，我们将RNAi表示为Minsky寄存器机器，使得（i）两个寄存器分别保存单链和双链RNA，以及（ii）机器的指令通过酶（Dicer）、siRNA（具有RISC复合物）和聚合（RdRp）与适当寄存器的相互作用来解释。将RNAi理解为一种计算结构，可以研究RNAi的计算意义，特别是它的复杂性。最初，机器被配置为化学接地形式（CGF），这会产生不正确的跳跃。为了解决这个问题，该系统被改造为递归RNAi，其中siRNA不仅靶向mRNA，还靶向Dicer和RISC的机器指令类似物。最后，研究了递归RNAi系统中的概率终止问题。
2012-11-17 cs.CE cs.LO q-bio.MN
The (In)Efficiency of Interaction
通过由交互的几何形状所启发的抽象机器来评估高阶函数程序已知会引起$\textit{space}$效率，代价是$\textit{time}$性能通常比传统的、基于环境的抽象机器所能获得的性能差。虽然确实存在前者比后者效率指数更低的非线性项族，但目前还不知道\emph{general}这种现象是如何发生的，以及在最坏的情况下，这种效率低下会持续多久。我们回答这些问题，制定四个不同的知名的抽象机器内一个共同的定义框架，这种方式能够给尖锐的相对时间效率的结果。我们还证明了非幂等交集类型论能够精确地反映交互式抽象机的时间性能，这种方式表明，它的时间效率低下，最终下降从高阶类型的存在。
2020-10-24 cs.LO cs.PL
A Complete Logic for Database Abstract State Machines
在数据库理论中，术语$\textit{database transformation}$用于指可计算查询和更新的统一处理。最近，有研究表明，非确定性数据库转换可以被ASM的一种变体准确捕获，即所谓的数据库抽象状态机（DB-ASM）。在这篇文章中，我们提出了一个DB-ASM的逻辑，扩展了Nanchen和Stärk的逻辑。特别是，我们开发了一个严格的证明系统的逻辑DB-ASMs，这是被证明是健全和完整的。扩展处理的最困难的挑战是一个适当的形式化捕获数据库转换的非确定性及其所有相关功能，如一致性，更新集或与DB-ASM规则相关的多集。由于数据库转换的状态的数据库部分是有限结构，并且DB-ASM通过仅允许状态的数据库部分上的量词来限制，因此我们通过将更新集显式地带入逻辑中来解决这个问题，即通过使用额外的模态运算符$[X]$，其中$X$被解释为由DB-ASM规则生成的更新集$Δ$。DB-ASM逻辑提供了一个强大的验证工具来研究数据库转换的属性。
2017-05-30 cs.LO
On Abstract Machine Semantics for Proto-Quipper-M
Quipper是一种用于描述量子电路的特定领域程序设计语言。因为它是作为Haskell中的嵌入式语言实现的，所以Quipper是一种非常实用的函数式语言。然而，出于同样的原因，它缺乏正式的语义，并且受到Haskell类型系统的限制。特别是，由于Haskell缺乏线性类型，很容易编写违反量子态不可克隆特性的Quipper程序。为了以类型安全的方式形式化Quipper的相关片段，在过去几年中引入了Proto-Quipper家族的研究语言。在本文中，我们首先回顾Proto-Quipper-M，Proto-Quipper家族的一个实例，它基于量子电路的分类模型，具有线性类型系统，保证了非克隆属性在编译时保持不变。然后，我们推导出一个试探性的小步操作语义的大步骤语义的Proto-Quipper-M，我们证明了这两个是等价的。在证明了试探性语义的主题缩减和进展结果后，我们在此基础上构建了一个真正的抽象机器风格的小步语义，我们最终证明了它与原始语义是等价的。
2021-05-07 cs.LO cs.PL quant-ph
Executable Behaviour and the π-Calculus (extended abstract)
反应式图灵机扩展了经典的图灵机，具有对可观察的交互行为进行建模的功能。当且仅当一个行为在行为上等价于反应式图灵机的行为时，我们称之为可执行行为。在本文中，我们研究的可执行行为和行为之间的关系，可以指定的π演算。我们建立了所有可执行的行为可以指定在π演算的分歧保持分支双相似性。然而，由于反应式图灵机模型的（预期的）限制，相反的情况是不正确的。也就是说，π演算允许指定的行为是不可执行的分歧保持分支双相似性。出于对可执行性的直观理解，我们考虑对与每个pi项可执行行为相关联的pi演算的操作语义的限制，至少到不需要保持发散的分支双相似性的版本。
2015-08-20 cs.LO
The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter
本文提出动态交互几何机器（DGoIM），结合令牌传递与图重写，统一研究空间与时间效率权衡，证明其对三种求值策略的可靠性和完备性，并归类为高效机器。
2019-10-29 cs.LO cs.PL
Behavioural Theory of Reflective Algorithms II: Reflective Parallel Algorithms
本文发展了能修改自身行为的反射并行算法的行为理论，包含定义RA类的公设、基于rASMs的抽象机器模型，并证明所有RA均可被该模型捕获。
2025-08-12 cs.LO
Exact Exploration
本文细化经典算法的步内行为分析，证明存在一种abstract state machine能精确复制给定算法的状态转移和状态测试，从而支持纳入状态仅部分定义相等性或使用原生部分函数的算法。
2024-10-14 cs.DS cs.LO cs.SE
Addressing Machines as models of lambda-calculus
本文提出可寻址机器作为λ演算模型，通过仅操作地址的简单机器及最左归约语义，并引入类似ω和ζ_β的规则，构建完整的无类型λ演算模型。
2022-07-28 cs.LO
A Diamond Machine For Strong Evaluation
本文提出一种用于 λ 演算强求值的新型 Diamond 抽象机器，通过拆分作业避免回溯，并利用 diamond 性质支持参数化调度与多种求值策略。
2023-10-01 cs.LO cs.PL
On Jumps, Interactions, and Intersection Types
Université Sorbonne Paris Nord（索邦巴黎北大学）；Università di Bologna（博洛尼亚大学）；Inria（法国国家信息与自动化研究所）；IRIF, Université Paris Cité（IRIF，巴黎西岱大学）
本文提出参数化跳跃抽象机（PaJAM），并证明其与非幂等交集类型之间的紧密对应，通过类型推导可提取计算步数，且通过限制回溯深度可统一经典模型。
2026-06-26 cs.LO
An Operational Foundation for Delimited Continuations in the CPS Hierarchy
本文为扩展了 shift/reset 控制算子的 lambda-calculus 提出抽象机和归约语义，以支持 CPS 层次中的定界续延，并展示其在列表前缀查找和求值归一化中的新应用。
2005-12-08 cs.LO cs.PL
