Impredicative Concurrent Abstract Predicates

DOI10.1007/978-3-642-54833-8_9zbMath1405.68092OpenAlexW75891272MaRDI QIDQ5410698

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

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

Related Items (30)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ Abstract local reasoning for concurrent libraries: mind the gap ⋮ On models of higher-order separation logic ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Caper ⋮ Verifying Concurrent Graph Algorithms ⋮ A perspective on specifying and verifying concurrent modules ⋮ Formally verifying exceptions for low-level code with separation logic ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Higher-order linearisability ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ A model of guarded recursion via generalised equilogical spaces ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ Steps in modular specifications for concurrent modules (invited tutorial paper) ⋮ A model of PCF in guarded type theory ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ A Light Modality for Recursion ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ The Essence of Higher-Order Concurrent Separation Logic ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Abstract Specifications for Concurrent Maps ⋮ Denotational semantics for guarded dependent type theory ⋮ Is Impredicativity Implicitly Implicit ⋮ Unnamed Item ⋮ Modular Termination Verification for Non-blocking Concurrency ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ Unnamed Item ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Unnamed Item

This page was built for publication: Impredicative Concurrent Abstract Predicates