Impredicative concurrent abstract predicates

DOI10.1007/978-3-642-54833-8_9MaRDI QIDQ5410698zbMATH OpenOpenAlexFDO

Authors Kasper Svendsen, Lars Birkedal

Publication date 16 April 2014

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-54833-8_9

Mathematics Subject Classification ID

Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Caper
• Modular reasoning about separation of concurrent data structures
• CONCUR 2004 - Concurrency Theory
• Modular reasoning for deterministic parallelism

Cited in

(31)

• A perspective on specifying and verifying concurrent modules
• Formally verifying exceptions for low-level code with separation logic
• Lewis meets Brouwer: constructive strict implication
• A model of guarded recursion via generalised equilogical spaces
• On models of higher-order separation logic
• Higher-order linearisability
• Modular termination verification for non-blocking concurrency
• Transfinite step-indexing: decoupling concrete and logical steps
• Guarded dependent type theory with coinductive types
• Abstract local reasoning for concurrent libraries: mind the gap
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Caper
• The essence of higher-order concurrent separation logic
• A higher-order logic for concurrent termination-preserving refinement
• Abstract specifications for concurrent maps
• Verifying concurrent graph algorithms
• Denotational semantics of recursive types in synthetic guarded domain theory
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Aneris: a mechanised logic for modular reasoning about distributed systems
• \textbf{Actris 2.0}: asynchronous session-type based reasoning in separation logic
• Higher-order linearisability
• Denotational semantics for guarded dependent type theory
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• A model of PCF in guarded type theory
• Is Impredicativity Implicitly Implicit
• Concise outlines for a complex logic: a proof outline checker for TaDA
• A logical approach to type soundness
• A compositional theory of linearizability
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Balancing expressiveness in formal approaches to concurrency

This page was built for publication: Impredicative concurrent abstract predicates

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5410698)