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

Mathematics Subject Classification ID

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)

On models of higher-order separation logic ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Coq

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