Argon, P., Mullins, J., & Roux, O. (juillet 1996). A correct compiler construction using Coq [Communication écrite]. Workshop on Proof Search in Type-Theoretic Languages (CADE 1996), New Brunswick, USA. Non disponible
