首页/论文/2002.05649

arXiv 2002.056492020-02cs.LOcs.PL

The Abstract Machinery of Interaction (Long Version)

Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

备注：: Accepted at PPDP 2020

英文摘要：

This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear logic proof nets, and whose soundness proof is convoluted and passes through various other formalisms. Here we provide a new direct proof of its correctness, based on a variant of Sands's improvements, a natural notion of bisimulation. Moreover, our proof is carried out on a new presentation of the IAM, defined as a machine acting directly on $λ$-terms, rather than on linear logic proof nets.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

堆交换性的抽象域（扩展版）

An Abstract Domain for Heap Commutativity (Extended Version)

本文提出一种面向堆操作程序的抽象域，将具体堆程序的交换性验证转移到抽象数学模型上安全执行，并支持框架化与组合推理，已在 Coq 中完成机械化。

2024-11-25cs.LOcs.PL

Topological representation of intuitionistic and distributive abstract logics

We continue work of our earlier paper (Lewitzka and Brunner: Minimally generated abstract logics, Logica Universalis 3(2), 2009), where abstract logics and particularly intuitionistic abstract logics are studied. Abstract logics can be topologized in a direct and natural way. This facilitates a topological study of classes of concrete logics whenever they are given in abstract form. Moreover, such a direct topological approach avoids the often complex algebraic and lattice-theoretic machinery usually applied to represent logics. Motivated by that point of view, we define in this paper the cate…

2015-08-18cs.LOmath.LO

Pretty-big-step-semantics-based Certified Abstract Interpretation（Preliminary version）

Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)

我们提出了一种技术，用于从自然语义规范的程序设计语言的语义程序分析。该技术基于一种特殊的语义，称为pretty-big-step语义。我们提出了一个漂亮的大步骤语义的语言与简单的对象称为O 'While，并指定了一系列的仪表的语义，明确了流程的值在程序中。这导致了基于语义的依赖性分析，在核心，例如，污染分析在软件安全中的应用用Coq证明助手实现了形式化。

2013-09-20cs.LOcs.PL

逻辑程序设计的交互语义

An interactive semantics of logic programming

我们适用于逻辑编程的一些最近出现的想法，从该领域的减少为基础的通信系统，目的是提供证据的隐藏的相互作用和协调机制，规则的运作机制，这样的编程范式。语义框架，我们选择了我们的结果是瓦片逻辑，它的优点是允许一个统一的治疗目标和意见，并应用抽象的分类工具来证明结果。作为主要的贡献，我们提到的有限表示的抽象统一，和并发和协调的抽象语义逻辑编程的最常见的语义相一致。此外，拼块语义的组合性由标准结果保证，因为它减少了对与逻辑程序相关联的拼块系统享有拼块分解属性的检查。还讨论了处理约束系统的方法的扩展。

2001-07-17cs.LOcs.PL

On Feller Continuity and Full Abstraction (Long Version)

We study the nature of applicative bisimilarity in $λ$-calculi endowed with operators for sampling from continuous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with contextual equivalence when real numbers can be manipulated only through continuous functions. The key ingredient towards this result is a novel notion of Feller-continuity for labelled Markov processes, which we believe of independent interest, being a broad class of LMPs for which coinductive and logically inspired equivalences coincide. On the other hand, we…

2022-07-21cs.LOcs.PL

$\pi$ 演算的一个内涵完全抽象层模型（扩展版）

An intensionally fully-abstract sheaf model for $π$ (expanded version)

本文为 $\pi$-演算提出基于简单站点上层的组合模型，该层对应并发无辜策略，并证明其内涵完全抽象于公平测试等价，核心是借助字符串图构造站点。

2017-11-14cs.LOcs.PL

更多相关论文收起更多论文

Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL* (Extended Version)

Variational systems allow effective building of many custom variants by using features (configuration options) to mark the variable functionality. In many of the applications, their quality assurance and formal verification are of paramount importance. Family-based model checking allows simultaneous verification of all variants of a variational system in a single run by exploiting the commonalities between the variants. Yet, its computational cost still greatly depends on the number of variants (often huge). In this work, we show how to achieve efficient family-based model checking of CTL* tem…

2018-03-05cs.LOcs.PLcs.SE

直觉主义版本匹配逻辑的完备海廷代数语义（扩展摘要）

Complete Heyting Algebra Semantics for an Intuitionistic Version of Matching Logic (Extended Abstract)

Research Center for Logic, Optimization and Security (LOS), University of Bucharest（布加勒斯特大学逻辑、优化与安全研究中心）；Institute for Logic and Data Science, Bucharest（布加勒斯特逻辑与数据科学研究所）

该研究推进直觉主义版本可应用匹配逻辑的构建，提出基于完备Heyting代数的语义框架，还设计了对应的证明系统并验证了其可靠性。

2026-09-28cs.LO

Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)

We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $λ$-calculi with algebraic effects. We first of all endow a computational $λ$-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract.

2017-04-15cs.LOcs.PL

通过抽象解释的程序验证实现模型检验（扩展版）

Model Checking as Program Verification by Abstract Interpretation (Extended Version)

本文提出将模型检验视为程序验证，引入MOKA语言把时序逻辑公式编码为程序，并结合抽象解释与局部完全抽象动态精化分析精度，从而复用更一般的抽象并避免误报。

2025-06-05cs.LO

A verified abstract machine for functional coroutines

Functional coroutines are a restricted form of control mechanism, where each coroutine is represented with both a continuation and an environment. This restriction was originally obtained by considering a constructive version of Parigot's classical natural deduction which is sound and complete for the Constant Domain logic. In this article, we present a refinement of de Groote's abstract machine for functional coroutines and we prove its correctness. Therefore, this abstract machine also provides a direct computational interpretation of the Constant Domain logic.

2016-06-21cs.LOcs.PL

Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)

Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated with the node that is computed as a fixpoi…

2017-11-09cs.DScs.LOcs.PL

非确定性情境演算动作理论的抽象——扩展版

Abstraction of Nondeterministic Situation Calculus Action Theories -- Extended Version

Ronin Institute（罗宁研究所）；University of Oxford（牛津大学）；York University（约克大学）

基于非确定性情境演算和ConGolog，提出一个通过细化映射连接抽象与具体动作理论的智能体行为抽象框架，支持策略推理与综合，并证明了抽象层面的强FOND计划可细化为具体层面的有效计划。

2023-05-20cs.AIcs.LO

超越反事实检验：基于实际因果的抽象论证反事实解释（扩展版）

Beyond But-for Test: Counterfactual Explanation in Abstract Argumentation via Actual Causality (Extended Version)

Zhejiang University（浙江大学）

针对抽象论证中的反事实解释问题，提出基于干预的反事实推理框架，通过编码论证接受条件为方程并定义干预算子，超越反事实检验，正确识别抢先和过度决定等结构中的原因。

2026-07-01cs.AIcs.LO

Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version

LibraBFT is a Byzantine Fault Tolerant (BFT) consensus protocol based on HotStuff. We present an abstract model of the protocol underlying HotStuff / LibraBFT, and formal, machine-checked proofs of their core correctness (safety) property and an extended condition that enables non-participating parties to verify committed results. (Liveness properties would be proved for specific implementations, not for the abstract model presented in this paper.) A key contribution is precisely defining assumptions about the behavior of honest peers, in an abstract way, independent of any particular implemen…

2022-03-29cs.DCcs.LO

关于跳跃、交互与交集类型

On Jumps, Interactions, and Intersection Types

Université Sorbonne Paris Nord（索邦巴黎北大学）；Università di Bologna（博洛尼亚大学）；Inria（法国国家信息与自动化研究所）；IRIF, Université Paris Cité（IRIF，巴黎西岱大学）

本文提出参数化跳跃抽象机（PaJAM），并证明其与非幂等交集类型之间的紧密对应，通过类型推导可提取计算步数，且通过限制回溯深度可统一经典模型。

2026-06-26cs.LO

Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (Extended Version)

This paper studies the quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value $λ$-calculus with a linear type system that can express programs sensitivity, enriched with algebraic operations \emph{à la} Plotkin and Power. To do so a general, abstract framework for studying behavioural relations taking values over quantales is defined according to Lawvere's analysis of generalised metric spaces. Barr's notion of relator (or lax extension) is then extended to quantale-valued relations adapting and extending resul…

2018-02-06cs.LO

Safety Verification and Refutation by k-invariants and k-induction (extended version)

Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checking, invariant inference in abstract interpretation and completeness via annotation for deductive verification. This creates a significant and fundamental usability problem as users may have to learn and use one technique to find potential problems but then need an entirely different one to show that they have been fixed. This paper presents a single, unified algorithm kIkI, which strictly…

2015-06-29cs.LOcs.SE