检索结果-内蒙古大学图书馆

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

作者： Stepanenko, Sergei Nardino, Emma Frumin, Dan Timany, Amin Birkedal, Lars Aarhus University Aarhus Denmark Univ Lyon ENS de Lyon UCBL CNRS Inria LIP UMR 5668 Lyon CEDEX 0769342 France University of Groningen Groningen Netherlands

ISBN: (纸本)9783031911200

Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects whose behaviors depend on the evaluation context, e.g., call/cc, shift and reset. Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called "bind rule" in modern program logics (which allows one to reason modularly about a term inside a context) is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles (and the Coq implementation) for context-independent effects remain the same. We show that our implementation of context-dependent effects is viable and powerful. We use it to give direct-style denotational semantics for higher-order programming languages with call/cc and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that the denotational semantics is adequate with respect to the operational semantics. This is achieved by constructing logical relations between syntax and semantics inside the program logic. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store. © The Author(s) 2025.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

A Program logic for Concurrent Randomized Programs in the Oblivious Adversary Model 34th

A Program Logic for Concurrent Randomized Programs in the Ob...

引用

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

作者： Fan, Weijie Liang, Hongjin Feng, Xinyu Jiang, Hanru State Key Laboratory for Novel Software Technology Nanjing University Jiangsu Nanjing210023 China Beijing Institute of Mathematical Sciences and Applications Beijing Beijing101408 China

ISBN: (纸本)9783031911170

Concurrent randomized programs in the oblivious adversary model are extremely difficult for modular verification because the interaction between threads is very sensitive to the program structure and the execution steps. We propose a new program logic supporting thread-local verification. With a novel "split" mechanism, one can split the state distribution into smaller partitions, and the reasoning can be done based on each partition independently, which allows us to avoid considering different execution paths of branch statements simultaneously. The logic rules are compositional and are natural extensions of their sequential counterparts. Using our program logic, we verify four typical algorithms in the oblivious adversary model. © The Author(s) 2025.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

On the Relationship between Dijkstra Monads and Higher-Order Fixpoint logic 34th

On the Relationship between Dijkstra Monads and Higher-Order...

引用

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

作者： Yamada, Risa Kobayashi, Naoki Sakayori, Ken Sato, Ryosuke The University of Tokyo Tokyo Japan Tokyo University of Agriculture and Technology Tokyo Japan

ISBN: (纸本)9783031911200

We study the relationship between two approaches to higher-order program verification: a semi-automated method using Dijkstra monads and a fully automated method using a higher-order fixpoint logic called HFL(Z). Although the origins of both approaches are quite different, there are some striking similarities: both convert programs to corresponding predicate transformers, and the conversion is essentially obtained by a CPS transformation. After reviewing the two approaches, we formalize an exact correspondence between the two for a restricted fragment of a functional language. We also point out that, outside the restricted fragment, there are some important differences between the two approaches, suggesting the need for cross-fertilization to obtain the best of the two approaches. As an example of the cross-fertilization, we also propose a semi-automated verification method, which requires less annotations than the Dijkstra monad approach and can scale to larger programs than the HFL(Z) approach. © The Author(s) 2025.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Split Decisions: Explicit Contexts for Substructural Languages 25

Split Decisions: Explicit Contexts for Substructural Languag...

引用

14th Conference on Certified Programs and Proofs

作者： Zackon, Daniel Sano, Chuta Momigliano, Alberto Pientka, Brigitte McGill Univ Montreal PQ Canada Univ Milan Milan Italy

ISBN: (纸本)9798400713477

A central challenge in mechanizing the meta-theory of substructural languages is modeling contexts. Although various ad hoc approaches to this problem exist, we lack a set of good practices and a simple infrastructure that can be leveraged for mechanizing a wide range of substructural systems. In this work, we describe Contexts as Resource Vectors (CARVe), a general syntactic infrastructure for managing substructural contexts, where elements are annotated with tags from a resource algebra denoting their availability. Assumptions persist as contexts are manipulated since we model resource consumption by changing their tags. We may thus define relations between substructural contexts via simultaneous substitutions without the need to split them. Moreover, we establish a series of algebraic properties about context operations that are typically required to carry out proofs in practice. CARVe is implemented in the proof assistant Beluga. To illustrate best practices for using our infrastructure, we give a detailed reformulation of the linear sequent calculus and bidirectional linear lambda-calculus in terms of CARVe's context operations and prove their equivalence using the aforementioned algebraic properties. In addition, we apply CARVe to mechanize a diverse set of systems, from the affine lambda-calculus to the session-typed process calculus CP, giving us confidence that CARVe is sufficiently general to mechanize a broad range of substructural systems.

关键词： mechanized meta-theory substructural type systems substructural logics linear logic verification

来源：评论

学校读者我要写书评

暂无评论

ASP-Based Multi-Shot Reasoning via DLV2 with Incremental Grounding

引用

theory and practice of logic programming 2025年

作者： Calimeri, Francesco Ianni, Giovambattista Pacenza, Francesco Perri, Simona Zangari, Jessica Univ Calabria Arcavacata Di Rende Italy

DLV2 is an AI tool for knowledge representation and reasoning that supports answer set programming (ASP) - a logic-based declarative formalism, successfully used in both academic and industrial applications. Given a logic program modeling a computational problem, an execution of DLV2 produces the so-called answer sets that correspond one-to-one to the solutions to the problem at hand. The computational process of DLV2 relies on the typical ground & solve approach, where the grounding step transforms the input program into a new, equivalent ground program, and the subsequent solving step applies propositional algorithms to search for the answer sets. Recently, emerging applications in contexts such as stream reasoning and event processing created a demand for multi-shot reasoning: here, the system is expected to be reactive while repeatedly executed over rapidly changing data. In this work, we present a new incremental reasoner obtained from the evolution of DLV2 toward iterated reasoning. Rather than restarting the computation from scratch, the system remains alive across repeated shots, and it incrementally handles the internal grounding process. At each shot, the system reuses previous computations for building and maintaining a large, more general ground program, from which a smaller yet equivalent portion is determined and used for computing answer sets. Notably, the incremental process is performed in a completely transparent fashion for the user. We describe the system, its usage, its applicability, and performance in some practically relevant domains.

关键词： knowledge representation and reasoning nonmonotonic reasoning logic programming answer set programming grounding stream reasoning

来源：评论

学校读者我要写书评

暂无评论

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration 34th

Compositional Shape Analysis with Shared Abduction and Biabd...

引用

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

作者： Sextl, Florian Rogalewicz, Adam Vojnar, Tomáš Zuleger, Florian Faculty of Informatics Institute of Logic and Computation TU Wien Vienna Austria Faculty of Information Technology Brno University of Technology Brno Czech Republic Faculty of Informatics Masaryk University Brno Czech Republic

ISBN: (纸本)9783031911200

Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of analysis;two of which we address in this paper. On the one hand, the original analysis is path-sensitive but cannot combine safety requirements for related branches. This causes the analysis to require additional soundness checks and decreases the analysis’ precision. We extend the underlying symbolic execution and propose a framework for shared abduction where a common pre-condition is maintained for related computation branches. On the other hand, prior implementations lift loop acceleration methods from forward analysis to biabduction analysis by applying them separately on the pre- and post-condition, which can lead to imprecise or even unsound acceleration results that do not form a loop invariant. In contrast, we propose biabductive loop acceleration, which explicitly constructs and checks candidate loop invariants. For this, we also introduce a novel heuristic called shape extrapolation. This heuristic takes advantage of locality in the handling of list-like data structures (which are the most common data structures found in low-level code) and jointly accelerates pre- and post-conditions by extrapolating the related shapes. In addition to making the analysis more precise, our techniques also make biabductive analysis more efficient since they are sound in just one analysis phase. In contrast, prior techniques always require two phases (as the first phase can produce contracts that are unsound and must hence be verified). We experimentally confirm that our techniques improve on prior techniques;both in terms of precision and runtime of the analysis. © The Author(s) 2025.

关键词： Biabduction Shape Analysis

来源：评论

学校读者我要写书评

暂无评论

In Praise of Impredicativity: A Contribution to the Formalization of Meta-programming

引用

theory and practice of logic programming 2020年第1期20卷 99-146页

作者： Bry, Francois Ludwig Maximilian Univ Munich Inst Informat Munich Germany

Processing programs as data is one of the successes of functional and logic programming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are called in logic programming, are widespread declarative programming techniques. In logic programming, there is a gap between the meta-programming practice and its theory: The formalizations of meta-programming do not explicitly address its impredicativity and are not fully adequate. This article aims at overcoming this unsatisfactory situation by discussing the relevance of impredicativity to meta-programming, by revisiting former formalizations of meta-programming, and by defining Reflective Predicate logic, a conservative extension of first-order logic, which provides a simple formalization of meta-programming.

关键词： logic programming meta-programming model theory Barber Paradox Russell's Paradox reflection

来源：评论

学校读者我要写书评

暂无评论

Introduction to the 30th International Conference on logic programming Special Issue

引用

theory and practice of logic programming 2014年第4-5期14卷 401-414页

作者： Leuschel, Michael Schrijvers, Tom Univ Dusseldorf Dusseldorf Germany Univ Ghent B-9000 Ghent Belgium

The 30th edition of the International Conference of logic programming took place in Vienna in July 2014 at the Vienna Summer of logic - the largest scientific conference in the history of logic. Following the initiative in 2010 taken by the Association for logic programming and Cambridge University Press, the full papers accepted for the International Conference on logic programming again appear as a special issue of theory and practice of logic programming (TPLP) - the 30th International Conference on logic programming Special Issue. Papers describing original, previously unpublished research and not simultaneously submitted for publication elsewhere were solicited in all areas of logic programming including but not restricted to: theory: Semantic Foundations, Formalisms, Non- monotonic Reasoning, Knowledge Representation; Implementation: Compilation, Memory Management, Virtual Machines, Parallelism; Environments: Program Analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing; Language Issues: Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, programming Techniques; Related Paradigms: Abductive logic programming, Inductive logic programming, Constraint logic programming, Answer-Set programming; Applications: Databases, Data Integration and Federation, Software Engineering, Natural Language Processing, Web and Semantic Web, Agents, Artificial Intelligence, Bioinformatics.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A Survey of the Proof-Theoretic Foundations of logic programming

引用

theory and practice of logic programming 2022年第6期22卷 859-904页

作者： Miller, Dale Ecole Polytech Inria Saclay Palaiseau France Ecole Polytech LIX Palaiseau France

Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this article, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

logic programming with default, weak and strict negations

引用

theory and practice of logic programming 2006年第0期6卷 737-749页

作者： Yamasaki, Susumu Okayama Univ Grad Sch Nat Sci & Technol Dept Comp Sci Okayama 7008530 Japan

This paper looks at logic programming with three kinds of negation: default, weak and strict negations. A 3-valued logic model theory is discussed for logic programs with three kinds of negation. The procedure is cons... 详细信息

关键词： negation in logic programming 3-valued logic

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：