This repository contains the Rocq development of the paper:
- Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 32nd IEEE Computer Security Foundations Symposium (CSF), pages 256--271. June 2019. Distinguished Paper Award.
The best entry point for this work is the appendix of the paper above, which includes direct pointers to various Rocq and text files.
The Rocq development is known to work with Rocq/Coq v8.7.X, v8.8.X, and v8.9.0, v0.9.0 but it has very few dependencies, so it will likely work with other versions as well.
$ make -j4
This Rocq development is licensed under the Apache License, Version 2.0 (see LICENSE).
This Rocq development's main contributors include Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault.