This page accompanies the paper Temporary Read-Only Permissions for Separation Logic by Arthur Charguéraud and François Pottier.
This self-contained archive contains TLC, CFML, and a model of Separation Logic with Read-Only Permissions. The requirements are OCaml and Coq 8.5.