Formalizing Determinacy of Concurrent Revisions
summary
Formalizes part of the 2011 concurrent revisions semantics in Isabelle formalization, proving determinacy (confluence modulo equivalence) by completing case analysis and adding a needed mimicking diagram to close squares; finds and fixes a real bug by strengthened freshness side condition while showing some allocation side conditions can be weakened, handles about 81 single-step cases in the strong local confluence proof, and publishes a machine-checked proof plus notes on remaining informal graph lemmas.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:21Properties
- 1:12Basic Concepts
- 2:56Version
- 3:24accumulative
- 3:58revision diagrams
- 4:48state of revision
- 6:05operational semantics
- 6:38revision identifiers
- 6:50notion of freshness
- 8:13realnew
- 10:43Determinacy
- 13:34Summary
related talks
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
19mBeyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
15mCompiling with Continuations, Correctly
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
21mChecking Equivalence in a Non-strict Language
15mClosing Remarks