Name: Programming Languages and Systems 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27–30, 2025, Proceedings (Alex Potanin) (z-library.sk, 1lib.sk, z-lib.sk)
Author: Unknown Author

Page 1

Potanin (E ds.) Program m ing Languages and System s Alex Potanin (Eds.) LN CS 1 62 01 Programming Languages and Systems APLAS 2025 23rd Asian Symposium, APLAS 2025 Bengaluru, India, October 27–30, 2025 Proceedings

Page 2

Lecture Notes in Computer Science 16201 Founding Editors Gerhard Goos Juris Hartmanis Editorial Board Members Elisa Bertino, Purdue University, West Lafayette, IN, USA Wen Gao, Peking University, Beijing, China Bernhard Steffen , TU Dortmund University, Dortmund, Germany Moti Yung , Columbia University, New York, NY, USA

Page 3

The series Lecture Notes in Computer Science (LNCS), including its subseries Lecture Notes in Artificial Intelligence (LNAI) and Lecture Notes in Bioinformatics (LNBI), has established itself as a medium for the publication of new developments in computer science and information technology research, teaching, and education. LNCS enjoys close cooperation with the computer science R & D community, the series counts many renowned academics among its volume editors and paper authors, and collaborates with prestigious societies. Its mission is to serve this international commu- nity by providing an invaluable service, mainly focused on the publication of conference and workshop proceedings and postproceedings. LNCS commenced publication in 1973.

Page 4

Alex Potanin Editor Programming Languages and Systems 23rd Asian Symposium, APLAS 2025 Bengaluru, India, October 27–30, 2025 Proceedings

Page 5

Editor Alex Potanin Australian National University Canberra, ACT, Australia ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notes in Computer Science ISBN 978-981-95-3584-2 ISBN 978-981-95-3585-9 (eBook) https://doi.org/10.1007/978-981-95-3585-9 © The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2026 This work is subject to copyright. All rights are solely and exclusively licensed by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. This Springer imprint is published by the registered company Springer Nature Singapore Pte Ltd. The registered company address is: 152 Beach Road, #21-01/04 Gateway East, Singapore 189721, Singapore If disposing of this product, please recycle the paper.

Page 6

Preface This volume contains the proceedings of the Twenty-Third Asian Symposium on Pro- gramming Languages and Systems – APLAS 2025 – held during October 27-29, 2025 in Bengaluru, India. APLAS brings together programming language researchers and practitioners and implementors worldwide, to present and discuss the latest results and exchange ideas in all areas of programming languages and systems. The list of topics includes, among others: programming paradigms and styles; methods and tools to specify and reason about programs and languages; programming language foundations; methods and tools for implementation; concurrency and distribution; applications and case studies. APLAS is organised by the Asian Association for the Foundation of Software (AAFS), founded by Asian researchers in cooperation with many researchers from Europe and the USA. Past APLAS symposiums were held in Kyoto (’24), Taipei (’23), Auckland (’22), Chicago (’21), Fukuoka (’20), Bali (’19), Wellington (’18), Suzhou (’17), Hanoi (’16), Pohang (’15), Singapore (’14), Melbourne (’13), Kyoto (’12), Kent- ing (’11), Shanghai (’10), Seoul (’09), Bangalore (’08), Singapore (’07), Sydney (’06), Tsukuba (’05), Taipei (’04) and Beijing (’03) after three informal workshops. The call for papers attracted 34 submissions, six of which were desk-rejected. The rest were reviewed double-blind: we aimed to keep the identities out of the picture during the whole review process. Each submission received three reviews. In addition, for some submissions, we sought opinions of external experts, whose prompt and very helpful comments were greatly appreciated. At the end of the review period, the authors had 3 days to respond to the reviews. The PC considered the responses and decided on acceptance. In many cases, the reviews were augmented to account for the responses and to summarise the PC discussion. Quite a number of responses clarified the submission and resolved the reviewers’ concerns. In some other cases, unfortunately, the responses did not address all the concerns and questions raised in the reviews. No numerical targets were set for acceptance. The only criterion was a submission being understandable, interesting and instructive to the audience and publishable in the proceedings, after perhaps only minor revisions. After careful and thorough discussions, The Program Committee accepted 13 submissions. The symposium program also included a plenary joint keynote with ATVA by Peter Müller (ETH Zurich, Switzerland). Furthermore, APLAS 2025 included a student research competition and a associated poster session, as well as the APLAS-NIER pre-conference workshop (Oct. 27, 2025). This year, APLAS was co-located with the 23rd International Symposium on Automated Technology for Verification and Analysis (ATVA). APLAS 2025 continued the tradition of recognising the best paper submitted to the symposium. I am delighted to announce that the Best Paper award for APLAS’25 went to:

Page 7

vi Preface Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu Positive Sharing and Abstract Machines Putting together APLAS 2025 was a team effort. First of all, I would like to thank the authors of the submitted papers and the presenters of the invited talks. Without the Program Committee, there would have been no program either, and I am very grateful to the PC members for their hard work. Complementing the PC were External Reviewers, whose contribution is gratefully acknowledged. I am indebted to the General Chair, Pritam Gharat (Microsoft Research India) for her support throughout the process. This year APLAS was held in co-operation with ATVA, whose organising committee – in particular, General Chair Deepak D’Souza, shared the burden. They have been invaluable in setting up the conference and making sure everything ran smoothly. Finally, thanks are due to the Award Sponsor Springer. September 2025 Alex Potanin

Page 8

Organization General Chair Pritam Gharat Microsoft Research, India Program Chair Alex Potanin Australian National University, Australia Program Committee Alex Potanin Australian National University, Australia Alexander Bakst Certora, USA Andrea Costea TU Delft, Netherlands Atsushi Igarashi Kyoto University, Japan Ganesan Ramalingam Microsoft, India Ina Schaefer Karlsruhe Institute of Technology, Germany Jeff Foster Tufts University, USA Kartik Nagar IIT Madras, India K. C. Sivaramakrishnan IIT Madras and Tarides, India Kihong Heo KAIST, South Korea Liam O’Connor Australian National University, Australia Lionel Parreaux Hong Kong University of Science and Technology, China Liyi Li Iowa State University, USA Manas Thakur IIT Bombay, India Meenakshi D’Souza International Institute of Information Technology Bangalore, India Oleg Kiselyov Tohoku University, Japan Pascal Weisenburger University of St Gallen, Switzerland Sanjiva Prasad IIT Delhi, India Stephen Kell King’s College London, UK Swarnendu Biswas IIT Kanpur, India Tachio Terauchi Waseda University, Japan Umang Mathur National University of Singapore, Singapore V. Krishna Nandivada IIT Madras, India

Page 9

viii Organization Zhenjiang Hu Peking University, China External Reviewers Andy Gordon, Daniele Varacca, Huan Zhao, Rujie Meng, Zihan Zhou

Page 10

Contents Type Systems, Safety, and Verification Memory Safety: Uniqueness as Separation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Pilar Selene Linares Arévalo, Arthur Azevedo de Amorim, Vincent Jackson, Liam O’Connor, Peter Schachte, and Christine Rizkallah Fair Termination for Resource-Aware Active Objects . . . . . . . . . . . . . . . . . . . . . . . 22 Francesco Dagnino, Paola Giannini, Violet Ka I Pun, and Ulises Torrella A Formal Foundation for Equational Reasoning on Probabilistic Programs . . . . . 44 Reynald Affeldt, Yoshihiro Ishiguro, and Zachary Stone Control, Effects, and Decidability Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 Ryunosuke Endo and Tachio Terauchi Expressive Power of One-Shot Control Operators and Coroutines . . . . . . . . . . . . 88 Kentaro Kobayashi and Yukiyoshi Kameyama Positive Sharing and Abstract Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Beniamino Accattoli, Claudio Sacerdoti Coen, and Jui-Hsuan Wu Quantum Programming and Logic IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 Kinnari Dave, Alejandro Díaz-Caro, and Vladimir Zamdzhiev A Quantum-Control Lambda-Calculus with Multiple Measurement Bases . . . . . 151 Alejandro Díaz-Caro and Nicolas A. Monzon Program Analysis, Specifications, and Decision Procedures Checking Consistency of Event-Driven Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173 Parosh Aziz Abdulla, Mohamed Faouzi Atig, R. Govind, Samuel Grahn, and Ramanathan S. Thinniyam

Page 11

x Contents Specification Inference Modulo Oracles for Database-Backed Web Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195 Nitesh Trivedi and Subhajit Roy Decision Procedure for a Theory of String Sequences . . . . . . . . . . . . . . . . . . . . . . . 217 Denghang Hu, Taolue Chen, Philipp Rümmer, Fu Song, and Zhilin Wu AI and Compiler Optimisation for Performance ELTC: An End-to-End Large Language Model-Based Tensor Compilation Optimization Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241 WenBo Ma, QingZeng Song, Fei Qiao, YongJiang Xue, and MingZe Sun Performance Optimization of HPC Workloads in Cloud Using AI-Driven Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 260 Aman Iftekhar and Rahul Mishra Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 275

Page 12

Type Systems, Safety, and Verification

Page 13

Memory Safety: Uniqueness as Separation Pilar Selene Linares Arévalo1(B) , Arthur Azevedo de Amorim2 , Vincent Jackson1 , Liam O’Connor3 , Peter Schac hte1 , and Christine Rizkallah1 1 The University of Melbourne, Melb ourne, VIC, Australia {linaresareva,v.jackson,schachte,christine.rizkallah}@unimelb.edu.au 2 Rochester Institute of Technology, Rochester, NY, USA 3 Australian National U niversity, Canberra, ACT, Australia liam.oconnor@anu.edu.au Abstract. Programming languages with uniqueness type systems pre- vent pointer aliasing, simplifying memory safety reasoning. However, code implemented in these languages often interoperates through foreign function interfaces with external components implemented in languages lacking the same level of static safety guarantees. To verify safe updates in a combined system, one must manually verify that the external com- ponents preserve the safety invariants of the uniqueness type system. In particular, recent work showed that one can manually discharge such obligations on C components from a cross-language Cogent-C system by directly reasoning about the C code in higher-order logic. However, even for simple examples, discharging the uniqueness safety obligations, known as frame conditions, within a logic not specifically designed for direct reasoning in terms of heaps and pointers was not ideal. Separation logic is an established logic that facilitates reasoning about imperative programs b y localising reasoning to the parts of the heap that the pro- gram mutates. This raises a vital question. Can we use separation logic to discharge the safety obligations imposed by uniqueness types? The answer is yes. This paper demonstrates that the frame conditions can be inferred from particular separation logic triples and, hence, discharged by reasoning using separation logic. We identify and verify the sound- ness of specific separation logic triples that imply the frame conditions imposed by a uniqueness type system. Keywords: Memory Safety · Uniqueness Type s · Separation Logic 1 Introduction Modern languages such as Clean [15], SaC [16], Mercury [18], and more recently, Cogent [9] leverage uniqueness type systems [17], a form of substructural type systems, to rule out the largest known class of common software vulnerabilities: memory safety errors. In particular, uniqueness types are typically used in these languages to prevent pointer aliasing : having multiple live references to the same c The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2026 A. Potanin (Ed.): APLAS 2025, LNCS 16201, pp. 3–21, 2026. https://doi.org/10.1007/978-981-95-3585-9_1

Page 14

4 P. S. Linares Arévalo et al. memory location. As such, they support the development of code that is safe by design and r emove the need for garbage collection, enabling efficient compilation. However, the safety guarantees of uniqueness typing are limited to code that adheres to the type system constraints. While the uniqueness condition is a con- ceptually simple restriction, it sometimes imposes a considerable burden when writing code in such languages. For example, a simple uniqueness type system would prohibit passing both an array and a reference to one of its elements to a function because of the aliasing this introduces, even if we only read from them, and no mutation is involved. Therefore, in practice, languages with uniqueness types often include an opt- out mechanism, to enable interoperation with external components written in unsafe fragments or unsafe languages, such as C, which do not enforce safety by design. This often involves using a f oreign function interface (FFI) to enable interoperation with surrounding infrastructure, such as system calls, and with existing components such as external libraries. For instance, SaC, a functional programming language with uniqueness types, provides an FFI to interoperate with external C libraries [5]. Similarly, the Cogent language [9] has an FFI to act as a bypass mechanism that enables in teroperation with C components. To verify the memory safety of a combined system, one must manually ver- ify that the external components preserve the invariants of the uniqueness type system that result in safety. Leaving these unverified could invalidate the guaran- tees obtained from using uniqueness types, even for the safe components. Recent work demonstrated that one can manually discharge such uniqueness conditions on C code in the context of a cross-language Cogent-C system, by directly rea- soning about the C code in higher-order logic. This shows that composing proo fs in such a cross-language setting is possible and that it is possible to discharge the uniqueness conditions on foreign code. However, even for a simple example, discharging uniqueness frame conditions in a logic not designed to verify such safety obligations was quite tedious [4]. These proofs should ideally be developed in a framework that facilitates reasoning about memory. One such framework is separation logic [14], a logic for reasoning about heap-manipulating programs that enables local reasoning about separate parts o f memory, through separating conjunction and the frame rule. This paper presents an imperative language with specific features for rea- soning about memory safety. In particular, we extend an existing imperative language [1] to distinguish memory safety errors from other type of errors and present a sound separation logic for this extension. Moreover, we present sepa- ration logic triples FC Triple and prove that they imply the uniqueness type invariants imposed by Cogent on foreign C code, on the shared heap between Cogent and C, called through Cogent’s FFI, which allows for verified interoper- ability of Cogent-C code [4]. We demonstrate that the FC Triple we identified can be discharged for a number of language constructs, including memory-related constructs. While the formal proofs do not form a contribution of this paper,

Page 15

Memory Safety: Uniqueness as Separation 5 our core results have been formalised in Rocq (formerly Coq) to gain higher confidence in our results. 2 Enforcing Uniqueness on Foreign Functions For this paper, we consider the memory safety invariants from Cogent, which is a functional programming language intended for low-level software and designed to write c ode in a safe, verifiable way without a garbage collector or heavy runtime [10]. Cogent’s uniqueness type system ensures exclusive ownership of mutable data, preventing aliasing and enabling direct updates without corrupting mem- ory. The uniqueness type system used in Cogent is quite sophisticated ( see the Cogent paper [10] for a full description); here, we only focus on the precise conditions under which external C code imported into C ogent, maintains the memory safety guarantees that its uniqueness types provide. Cogent’s typing relation tracks a set of pointers w transitively accessible through a value v, called the heap footprint—note that w is a subset of the domain of the current heap. Written v : τ w , this judgement states that v has type τ and a n associated footprint w. By annotating the relation in this way, the required non-aliasing requirements can be included in the typing rules. For example, the rule for typing tuples is: x : τ1 wx y : τ2 wy wx ∩ wy = ∅ (x, y) : τ1 × τ2 wx ∪ wy The disjointness condition wx∩wy = ∅ prevents internal aliasing in non-abstract structures, preserving the uniqueness guarantee. For abstract types implemented in C, however, internal aliasing may occur without breaking the uniqueness guar- antee. This is permissible because the type system enforces uniqueness at the abstract interface level, not within the hidden implementation. Let f : τ → ρ be a function implemented in C and imported into Cogent. Let v be the input value such that v : τ wi , hi the initial heap (a partial map from pointers to values), and f(v) the result such that f(v) : ρ wo with final heap ho. For f to respect the uniqueness invariants, the following frame conditions must hold: Leak Freedom ∀p. p ∈ wi ∧ p /∈ wo −→ p /∈ dom(ho), that is, any pointer in the input footprint that is not in the domain of the final heap must not appear in the initial heap. We use the equivalent yet more convenient formulation: wi ∩ dom(ho) ⊆ wo. Fresh Allocation ∀p. p /∈ wi ∧ p ∈ wo −→ p /∈ dom(hi), that is, any pointer in the output footprint that is not in the input footprint must not alias with any pointer in the initial heap. We use the equivalent yet more convenient formulation: wo ∩ dom(hi) ⊆ wi.

Page 16

6 P. S. Linares Arévalo et al. Inertia ∀p. p /∈ wi ∧ p /∈ wo −→ hi(p) = ho(p), that is, any part of the heap not in the input or output footprint remains unchanged. These conditions ensure that the function only relies on the memory it is permitted to access. Collectively, they are called the frame conditions, named after the frame problem in knowledge representation [8]. Manually discharging these proof obligations for external C code without the support of a suitable logic for reasoning about state is tedious [4]. The next sections will explain how these conditions can b e verified using separation logic [14], which is specifically designed for r easoning about heap-manipulating programs. 3 Language Syntax and Operational Semantics We introduce a simple imperative language LIMP for which we will define our separation logic. We adopt an imperative language [1] that captures key features of low-level memory manipulation: heap allocation and deallocation as well as reads and writes from and into the heap. This language is mechanised in Rocq, and it was used to define a formal notion of memory safety. As such, it provides a solid foundation for our work. We extend the language to distinguish memory- related errors from other errors. Fig. 1. Syntax Figure 1 presents the syntax of the extended language and supporting com- ponents. It features values v that include booleans, naturals, and pointers. A pointer is a pair (id , n) where id is a block identifier drawn from a countably infinite set I of memory identifiers, and n ∈ N is an offset. The distinguished value nil represents the result of an ill-typed expression (e.g., 3 + true) and is used to uniformly propagate errors. The language has standard expressions e that have no side effects on the state, including offset e, which returns the offset of a pointer value. It also features standard imperative commands c such as skip, local assignment, heap operations, and control flow constructs including

Page 17

Memory Safety: Uniqueness as Separation 7 loops. Figure 1 also presents the definition of states on which commands evalu- ate. States consist of a pair of components: a local store l, a finite partial map from variables to v alues, and a heap h, a finite partial map from pointers to values. Fig. 2. Evaluation of expressions (excerpt). Now that we have presented the syntax, let’s define an operational semantics for evaluating expressions and commands. Expression evaluation, e e : S → V, depends only on the local store. Hence, pointers may not be dereferenced in an expression. Base values, such as booleans, naturals, and nil, evaluate to them- selves. Arithmetic and boolean operations behave in the standard way. Addition and subtraction can additionally be used for performing pointer arithmetic on pointer offsets; we use the notation (i, n1) +p n2 as shorthand for the pointer addition (i, n1 + n2). Equalit y comparison is allowed on all values, with pointer equality comparing both the block identifier and offset. The ≤ operator applies only to naturals. Any operation applied to ill-typed values returns nil. Expres- sion evaluation is standard, and an excerpt of the expression evaluation function is presented in Fig. 2.

Page 18

8 P. S. Linares Arévalo et al. Fig. 3. Evaluation of commands

Page 19

Memory Safety: Uniqueness as Separation 9 The function − : C → N → S → R defines big-step evaluation for com- mands. It evaluates a program c in a given state s, with a maximum of n execu- tion steps, and produces a result. The result is either done s with final state s , an error error err, which could be a memory-related error m or an other error, or a t imeout result notYet if the execution limit n is reached before completion. Note that the number of steps n provided as fuel is a formalisation detail that is only necessary to conveniently formalise this semantics as a total function in Rocq. The language enforces safety by raising errors that immediately halt execu- tion, preventing undefined or unpredictable behaviour due to memory misuse. The command evaluation function is presented in Fig. 3. Unlike the original lan- guage semantics [1], our semantics distinguishes memory safety errors from other runtime errors. This distinction is necessary to define a separation logic validity triple that is sensitive to memory safety violations. Specifically, we extend the semantics to support the following memory safety errors: invalidRead, reading from an invalid memory location, invalidWrite, writing outside the bounds of a block or to otherwise invalid memory, invalidFree, freeing an invalid pointer. The evaluation follows the standard imperative semantics for skip, seq c1 c2, x := e, if e then c1 else c2, and while e do c. The load x e heap lookup command first evaluates e to a pointer and then attempts to read from that location in the heap. If e does not evaluate to a pointer, evaluation results in error other. If the pointer is invalid, either because the block identifier is not allocated or the offset is out of bounds, the result is an invalidRead error. Similarly, the heap mutation command, store e1 e2, requires e1 to evaluate to a valid pointer. If not, evaluation results in an invalidWrite error. The allocation command, alloc x e, evaluates e to a natural k and then produces a fresh block identifier that is not currently in use. A new block of size k is added to the heap, with all cells initialised to 0. This initialisation is important for ensuring that allocation does not leak information present in blocks that have b een previously freed. The resulting state binds x to a pointer that refers to the first cell in the new block. Block identifiers in this language are immutable once assigned, making it impossible to fabricate a pointer to an allocated block. The heap deallocation command, free e, evaluates e to a pointer. If the pointer is valid, the result is a heap where all cells associated with the corresponding block identifier are removed. If the pointer is invalid, evaluation results in an invalidFree error. To summarise, our semantics extends an existing imperative language with manual memory management [1] that was formalised in Rocq, by explicitly distinguishing memory safety violations from other errors. In the next section, we present a separation logic for reasoning abo ut this language and prove its soundness with respect to the operational semantics described here. 4 Separation Logic Now that we have defined the language and its operational semantics, we are ready to develop a separation logic for reasoning about programs in this lan- guage.

Page 20

10 P. S. Linares Arévalo et al. In standard separation logic [14], a triple (P, c, Q) is considered valid if whenever command c evaluates from a state satisfying precondition P , if eval- uation terminates, it does so successfully in a state satisfying postcondition Q. In particular, this notion of strong validity {P} c {Q}S holds exactly when ∀s k. P s → ( c k s = error err)∧ (∀s . c k s = done s → Qs ). That is, for any state s satisfying P , the execution of the program c in s will not trigger an error and, if the execution terminates, it will do so in a state satisfying Q. As previously observed in the literature [1], strong validity makes it difficult to distinguish reasoning about the validity of heap-related behaviour. For example, the triple {emp} free true {emp}S (where emp denotes the predicate that holds on states with an empty heap) is invalid, even though it accurately describes the behaviour of the heap: when the program runs on an empty heap, we obtain an error. However, when the program stops, the heap remains empty. To address this issue, a more permissive variant of separation logic allow- ing certain classes of errors was introduced [1], where weak validity, written {P} c {Q}W, holds if evaluating c from a state satisfying P either diverges, trig- gers an error, or terminates in a state satisfying Q. Formally, {P} c {Q}W holds iff ∀s k. P s → ( ∀s . c k s = done s → Q s ). Note that, under weak validity, {emp} free true {emp}S holds. However, this relaxed notion of validity introduces two major drawbacks. First, it in validates the soundness of the frame rule1, which is an essential com- ponent of separation logic, enabling the extension of local reasoning to parts of the heap that the command has not modified. Second, it is insensitive to the par- ticular error that has occurred. In this way, it undermines efforts to c haracterise memory-safe programs: for instance, {emp} load x e {emp}W is deemed valid, even though the command may raise a memory safety error. To remedy this, we introduce a third notion of validity that explicitly dis- tinguishes memory safety violations from other kinds of errors. A memory-safe validity triple, written {P} c {Q}M, holds if evaluating c from a state satisfying P does not result in a memory safety error and if it terminates successfully, the resulting state satisfies Q. In particular, memory-safe validity {P} c {Q}M holds iff ∀s k. P s → ( c k s = errorm) ∧ (∀s . c k s = done s → Qs ). All other behaviour, including divergence or non-memory-related errors, is permitted. This definition achieves the desired balance: it rejects {emp} load x e {emp}M as invalid reads violate memory safety; on the other hand, since the evaluation results in a non-memory-related error, {emp} free true {emp}S is a valid triple. An added benefit of this notion is that it turns out that it preserves the sound- ness of the frame rule, enabling modular reasoning about heap-manipulating programs u sing the standard frame rule. Since this separation logic triple is the one we focus on in this paper, we simply refer to it as {P} c {Q} in the rest of the paper. Before introducing the assertion logic used to describe program predicates, we first present the basic notation that underpins our logic (see Fig. 4). We write set disjointness as #; this holds when two sets have no elements in common. Heap 1 A detailed explanation of this issue can be found at the end of this section.

Programming Languages and Systems 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27–30, 2025, Proceedings (Alex Potanin) (z-library.sk, 1lib.sk, z-lib.sk)

Programming Languages and Systems 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27–30, 2025, Proceedings (Alex Potanin) (z-library.sk, 1lib.sk, z-lib.sk)

Registered users can read the full content for free

AI Reading Assistant

Passage locations

Support Author

Recommended for You