This repo contains the Coq development of the paper
- Trace-relating compiler correctness and secure compilation. Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Adrien Durier, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault. To appear at ESOP 2020.
The Coq development is known to work with Coq v8.8.X and v8.9.X, and requires the following Coq library:
- Mathematical Components 1.8.0 or 1.9.0
$ make -j4
This Coq development is licensed under the Apache License, Version 2.0 (see
LICENSE) unless overridden by another license file.