A Verified Algorithm for Detecting Conflicts in XACML Access
Control Rules, by Michel St-Martin and Amy P. Felty,
In Proceedings of the Fifth ACM SIGPLAN Conference on Certified
Programs and Proofs (CPP), 2016
The files run in Coq V8.4.
They must be compiled in the order they are listed.
The code is also available as a zip file.