Skip to content
Snippets Groups Projects
Forked from Iris / stdpp
Source project has a limited visibility.
  • Robbert Krebbers's avatar
    415a4f1c
    Support sequence point, add permissions, and update prelude. · 415a4f1c
    Robbert Krebbers authored
    Both the operational and axiomatic semantics are extended with sequence points
    and a permission system based on fractional permissions. In order to achieve
    this, the memory model has been completely revised, and is now built on top
    of an abstract interface for permissions.
    
    Apart from these changed, the library on lists and sets has been heavily
    extended, and minor changed have been made to other parts of the prelude.
    415a4f1c
    History
    Support sequence point, add permissions, and update prelude.
    Robbert Krebbers authored
    Both the operational and axiomatic semantics are extended with sequence points
    and a permission system based on fractional permissions. In order to achieve
    this, the memory model has been completely revised, and is now built on top
    of an abstract interface for permissions.
    
    Apart from these changed, the library on lists and sets has been heavily
    extended, and minor changed have been made to other parts of the prelude.