A higher-order logic for concurrent termination-preserving refinement
From MaRDI portal
Logic in computer science (03B70) Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.
Recommendations
- Compositional verification of termination-preserving refinement of concurrent programs
- Interactive proofs in higher-order concurrent separation logic
- Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
- A relational model of types-and-effects in higher-order concurrent separation logic
- ReLoC: a mechanised relational logic for fine-grained concurrency
Cites work
- A higher-order logic for concurrent termination-preserving refinement
- A Marriage of Rely/Guarantee and Separation Logic
- A program logic for concurrent objects under fair scheduling
- A relational model of types-and-effects in higher-order concurrent separation logic
- Behavioral polymorphism and parametricity in session-based communication
- BI as an assertion language for mutable data structures
- Communicating state transition systems for fine-grained concurrent resources
- Compositional verification of termination-preserving refinement of concurrent programs
- Higher-order ghost state
- Higher-order processes, functions, and sessions: a monadic integration
- scientific article; zbMATH DE number 3735115 (Why is no real title available?)
- scientific article; zbMATH DE number 7441269 (Why is no real title available?)
- Impredicative concurrent abstract predicates
- Interactive proofs in higher-order concurrent separation logic
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Linear logical relations for session-based concurrency
- Linear type theory for asynchronous session types
- Local rely-guarantee reasoning
- Modular termination verification for non-blocking concurrency
- Propositions as sessions
- Quantitative reasoning for proving lock-freedom
- Relational separation logic
- Resources, concurrency, and local reasoning
- Session types as intuitionistic linear propositions
- Simple relational correctness proofs for static analyses and program transformations
- Step-indexed relational reasoning for countable nondeterminism
- Tentative steps toward a development method for interfering programs
- The category-theoretic solution of recursive metric-space equations
- Transfinite step-indexing: decoupling concrete and logical steps
- Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
- Variables as resource for shared-memory programs: semantics and soundness
- Views, compositional reasoning for concurrent programs
Cited in
(16)- On models of higher-order separation logic
- A higher-order logic for concurrent termination-preserving refinement
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Compositional verification of termination-preserving refinement of concurrent programs
- \textbf{Actris 2.0}: asynchronous session-type based reasoning in separation logic
- ReLoC: a mechanised relational logic for fine-grained concurrency
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
- A relational model of types-and-effects in higher-order concurrent separation logic
- Completeness of asynchronous session tree subtyping in Coq
- A logical approach to type soundness
- Less is more revisited: association with global protocols and multiparty sessions
- Certified implementability of global multiparty protocols
- Formalising subject reduction and progress for multiparty session processes
- Inductive predicates via least fixpoints in higher-order separation logic
- Formalising asynchronous session subtyping
This page was built for publication: A higher-order logic for concurrent termination-preserving refinement
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988673)
