Unified Fine-grained Region Logic

Region logic and separation logic are two of the approaches to solving the frame problem. This project formalizes supported separation logic, and the fine-grained region logic in the KIV theorem prover.

This project defines the semantics of intuitionistic separation logic in terms of a global heap and regions, i.e., splitting and recombining heaps are achieved by region operations.

It proves that the new definition is equivalent to the one in Parkinson’s work.

This project proved that supported separation logic can be encoded into the fine-grained region logic.