ReLoC

DOI10.1145/3209108.3209174zbMath1497.68337OpenAlexW2798618564WikidataQ130855340 ScholiaQ130855340MaRDI QIDQ5145319

Robbert Krebbers, Dan Frumin, Lars Birkedal

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3209108.3209174

zbMATH Keywords

separation logiclogical relationsatomicityfine-grained concurrencyIris

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (4)

Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Decomposing data structure commutativity proofs with \(mn\)-differencing ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: ReLoC