References

1. Alfred V. Aho, Monica S. Lam, Ravi Sethi & Jeffrey D. Ullman (2006): Compilers: Principles, Techniques, and Tools (2Nd Edition). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.
2. Martin Clochard & Léon Gondelman (2015): Double WP : Vers une preuve automatique d'un compilateur. In: Journées Francophones des Langages Applicatifs, Val d'Ajol, France, pp. 1–18. Available at https://hal.inria.fr/hal-01094488.
3. Jean-Christophe Filliâtre & Martin Clochard (2013): A tiny register allocator for tree expressions. http://toccata.lri.fr/gallery/register_allocation.en.html. Online; accessed May 15th 2018.
4. Sabine Glesner, Simone Forster & Matthias Jäger (2005): A Program Result Checker for the Lexical Analysis of the GNU C Compiler. Electr. Notes Theor. Comput. Sci. 132(1), pp. 19–35, doi:10.1016/j.entcs.2005.01.029.
5. Léon Gondelman & Martin Clochard (2013): Double WP. http://toccata.lri.fr/gallery/double_wp.en.html. Online; accessed May 15th 2018.
6. Jason Hickey, Anil Madhavapeddy & Yaron Minsky (2014): Real World OCaml. "O'Reilly Media, Inc.". Available at http://www.worldcat.org/isbn/144932391.
7. Inria (2013): Why3 - Home. http://why3.lri.fr/. Online; accessed May 15th 2018.
8. Xavier Leroy (2009): Formal verification of a realistic compiler. Communications of the ACM 52(7), pp. 107–115, doi:10.1145/1538788.1538814. Available at http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf.
9. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin & Steve Zdancewic (2012): Formalizing the LLVM intermediate representation for verified program transformations.. In: John Field & Michael Hicks: POPL. ACM, pp. 427–440, doi:10.1145/2103656.2103709. Available at http://dblp.uni-trier.de/db/conf/popl/popl2012.html#ZhaoNMZ12.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org