# 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.