Separation Logic and Mutability

This is an in-progress formalisation of a short paper on an extension of Separation Logic for describing mutability.

It contains:

• a formalisation of Separation Logic from first principles, described in the src/SeparationLogic folder.
• a formalisation of the mutability extension, based on the original Separation Logic, described in the src/SeparationLogicWithMutability folder.