The Essence of Higher-Order Concurrent Separation Logic (Q2988664): Difference between revisions

@@ Property / author @@
+Lars Birkedal
@@ Property / author: Lars Birkedal / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Toolchain
@@ Property / describes a project that uses: Toolchain / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-662-54434-1_26
+Normal rank
@@ Property / OpenAlex ID @@
+W2596377803
@@ Property / OpenAlex ID: W2596377803 / rank @@
+Normal rank
@@ Property / cites work @@
+A very modal model of a modern, major, general type system
+Normal rank
@@ Property / cites work @@
+Program Logics for Certified Compilers
@@ Property / cites work: Program Logics for Certified Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+Proving assertions about parallel programs
@@ Property / cites work: Proving assertions about parallel programs / rank @@
+Normal rank
@@ Property / cites work @@
+Verified Compilation for Shared-Memory C
@@ Property / cites work: Verified Compilation for Shared-Memory C / rank @@
+Normal rank
@@ Property / cites work @@
+Permission accounting in separation logic
@@ Property / cites work: Permission accounting in separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4813391
@@ Property / cites work: Q4813391 / rank @@
+Normal rank
@@ Property / cites work @@
+Guarded commands, nondeterminacy and formal derivation of programs
+Normal rank
@@ Property / cites work @@
+Deny-Guarantee Reasoning
@@ Property / cites work: Deny-Guarantee Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+A relational modal logic for higher-order stateful ADTs
+Normal rank
@@ Property / cites work @@
+Oracle Semantics for Concurrent Separation Logic
@@ Property / cites work: Oracle Semantics for Concurrent Separation Logic / rank @@
+Normal rank
@@ Property / cites work @@
+BI as an assertion language for mutable data structures
+Normal rank
@@ Property / cites work @@
+Expressive modular fine-grained concurrency specification
+Normal rank
@@ Property / cites work @@
+Higher-order ghost state
@@ Property / cites work: Higher-order ghost state / rank @@
+Normal rank
@@ Property / cites work @@
+Iris
@@ Property / cites work: Iris / rank @@
+Normal rank
@@ Property / cites work @@
+Monads on symmetric monoidal closed categories
@@ Property / cites work: Monads on symmetric monoidal closed categories / rank @@
+Normal rank
@@ Property / cites work @@
+Strong functors and monoidal monads
@@ Property / cites work: Strong functors and monoidal monads / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive proofs in higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+A relational model of types-and-effects in higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+Resources, concurrency, and local reasoning
@@ Property / cites work: Resources, concurrency, and local reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+The Logic of Bunched Implications
@@ Property / cites work: The Logic of Bunched Implications / rank @@
+Normal rank
@@ Property / cites work @@
+Impredicative Concurrent Abstract Predicates
@@ Property / cites work: Impredicative Concurrent Abstract Predicates / rank @@
+Normal rank
@@ Property / cites work @@
+Modular Reasoning about Separation of Concurrent Data Structures
+Normal rank
@@ Property / cites work @@
+Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
+Normal rank