Published in

Association for Computing Machinery (ACM), Proceedings of the ACM on Programming Languages, POPL(5), p. 1-24, 2021

DOI: 10.1145/3434321



Export citation

Search in Google Scholar

Verified code generation for the polyhedral model

Journal article published in 2021 by Nathanaël Courant, Xavier Leroy
This paper is made freely available by the publisher.
This paper is made freely available by the publisher.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Green circle
Published version: archiving allowed
Data provided by SHERPA/RoMEO


The polyhedral model is a high-level intermediate representation for loop nests that supports elegantly a great many loop optimizations. In a compiler, after polyhedral loop optimizations have been performed, it is necessary and difficult to regenerate sequential or parallel loop nests before continuing compilation. This paper reports on the formalization and proof of semantic preservation of such a code generator that produces sequential code from a polyhedral representation. The formalization and proofs are mechanized using the Coq proof assistant.