Conditional Contextual Refinement

on YouTube ↗24m

" summary

A new refinement notion, Conditional Contextual Refinement (CCR), combines separation-logic pre/post conditions with transitive contextual refinement by inserting wrappers that operationalize specs and then proving a wrapper elimination theorem that removes them after linking. CCR uses demonic and angelic non-determinism to implicitly pass ownership resources without changing APIs, models separation assertions as predicates over explicit resources, and is implemented in Coq and evaluated on examples with shared memory, recursion, function pointers, non-termination and end-to-end assembly.

AI-written summary · about

" chapters (7)

1. 0:00Intro
2. 0:40Separation Logic vs. Refinement
3. 3:30Wait... what about: Relational Separation Logic
4. 9:07Motivating Example With Conditional Contextual Refinement
5. 11:17Stateless Conditional Refinement
6. 16:09Dual Non-Determinism Pass Resources Implicitly
7. 18:46Wrapper Elimination Theorem (WET)