A Higher-Order Logic for Concurrent Termination-Preserving Refinement
DOI10.1007/978-3-662-54434-1_34zbMath1485.68076arXiv1701.05888OpenAlexW2581223864MaRDI QIDQ2988673
Robert Harper, Joseph Tassarotti, Ralf Jung
Publication date: 19 May 2017
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1701.05888
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (5)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The category-theoretic solution of recursive metric-space equations
- Resources, concurrency, and local reasoning
- Relational separation logic
- Modular Termination Verification for Non-blocking Concurrency
- Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
- Iris
- A program logic for concurrent objects under fair scheduling
- Step-Indexed Relational Reasoning for Countable Nondeterminism
- Propositions as sessions
- Linear Logical Relations for Session-Based Concurrency
- Views
- Higher-order ghost state
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement
- Simple relational correctness proofs for static analyses and program transformations
- A Marriage of Rely/Guarantee and Separation Logic
- Session Types as Intuitionistic Linear Propositions
- Tentative steps toward a development method for interfering programs
- Compositional verification of termination-preserving refinement of concurrent programs
- BI as an assertion language for mutable data structures
- Linear type theory for asynchronous session types
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
- Local rely-guarantee reasoning
- Quantitative Reasoning for Proving Lock-Freedom
- Behavioral Polymorphism and Parametricity in Session-Based Communication
- Higher-Order Processes, Functions, and Sessions: A Monadic Integration
- Interactive proofs in higher-order concurrent separation logic
- A relational model of types-and-effects in higher-order concurrent separation logic
- Impredicative Concurrent Abstract Predicates
- Communicating State Transition Systems for Fine-Grained Concurrent Resources
This page was built for publication: A Higher-Order Logic for Concurrent Termination-Preserving Refinement
