_CoqProject · 25abf0a2a4e93f1ae9cb63f6a5264e2753463164 · Pierre Roux / Iris

Forked from Iris / Iris

Source project has a limited visibility.

4 years ago

Implement monotone partial bijections as a view · 25abf0a2

Tej Chajed authored 4 years ago

This is an alternative to !91, which was written prior to views. Using
the view CMRA we factor the implementation into purely algebraic library
and a logic-level wrapper. The logic-level wrapper exports resources
which seal away the underlying ownership and has theorems which handle
the ownership reasoning.

25abf0a2

History

Implement monotone partial bijections as a view

Tej Chajed authored 4 years ago

This is an alternative to !91, which was written prior to views. Using
the view CMRA we factor the implementation into purely algebraic library
and a logic-level wrapper. The logic-level wrapper exports resources
which seal away the underlying ownership and has theorems which handle
the ownership reasoning.