Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Trace Based Semantics for Rely...

view this post on Zulip Email Gateway (Aug 26 2026 at 08:45):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Trace Based Semantics for Rely Guarantee

TraceBasedSemantics forRelyGuarantee
<https://isa-afp.org/entries/Trace_Based_Rely_Guarantee.html>

Marialena Hadjikosti <https://isa-afp.org/authors/hadjikosti/>,Andrei
Popescu <https://isa-afp.org/authors/popescu/>andJamie Wright
<https://isa-afp.org/authors/wright/>

August 11, 2026

Abstract

We formalize a trace-based Rely-Guarantee semantics based on the work of
Xu et al. The foundation includes an abstract Sequential/While/Parallel
programming language equipped with operational semantics designed for
concurrent reasoning. Upon this, we build a reasoning infrastructure
that includes Rely-Guarantee inversion rules, alongside abstract
definitions and standard soundness proofs for both unary and binary
settings.

Enjoy!

Last updated: Sep 02 2026 at 16:10 UTC