{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T17:05:26Z","timestamp":1751648726986,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3434321","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Verified code generation for the polyhedral model"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8736-3060","authenticated-orcid":false,"given":"Nathana\u00ebl","family":"Courant","sequence":"first","affiliation":[{"name":"Inria, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8971-9171","authenticated-orcid":false,"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[{"name":"Coll\u00e8ge de France, France \/ PSL University, France"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/109625.109631"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2019.8661197"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.05.004"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2004.11"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666357.2597818"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/PGEC.1966.264565"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.1998.727127"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2018.00014"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254123"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_2_2_11_1","volume-title":"IMPACT 2012 : 2nd International Workshop on Polyhedral Compilation Techniques. https: \/\/hal.inria.fr\/hal-00655485","author":"Parrino Bruno Cuervo","year":"2012","unstructured":"Bruno Cuervo Parrino , Julien Narboux , Eric Violard , and Nicolas Magaud . 2012 . Dealing with arithmetic overflows in the polyhedral model . In IMPACT 2012 : 2nd International Workshop on Polyhedral Compilation Techniques. https: \/\/hal.inria.fr\/hal-00655485 Bruno Cuervo Parrino, Julien Narboux, Eric Violard, and Nicolas Magaud. 2012. Dealing with arithmetic overflows in the polyhedral model. In IMPACT 2012 : 2nd International Workshop on Polyhedral Compilation Techniques. https: \/\/hal.inria.fr\/hal-00655485"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01407931"},{"volume-title":"Encyclopedia of Parallel Programming","author":"Feautrier Paul","key":"e_1_2_2_13_1","unstructured":"Paul Feautrier and Christian Lengauer . 2011. The Polyhedron Model . In Encyclopedia of Parallel Programming , David Padua (Ed.). Springer , 1581-1592. Paul Feautrier and Christian Lengauer. 2011. The Polyhedron Model. In Encyclopedia of Parallel Programming, David Padua (Ed.). Springer, 1581-1592."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12154-3_13"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626412500107"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2743016"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360827.360844"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/109625.109630"},{"key":"e_1_2_2_23_1","unstructured":"Steven S. Muchnick. 1997. Advanced compiler design and implementation. Morgan Kaufmann.  Steven S. Muchnick. 1997. Advanced compiler design and implementation. Morgan Kaufmann."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_19"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_2_2_26_1","unstructured":"Alexandre Pilkiewicz. 2010-2013. s2sLoop: a validator for polyhedral transformations. ( 2010-2013 ). https:\/\/github.com\/ pilki\/s2sLoop  Alexandre Pilkiewicz. 2010-2013. s2sLoop: a validator for polyhedral transformations. ( 2010-2013 ). https:\/\/github.com\/ pilki\/s2sLoop"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/109025.109108"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007554627716"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3150211"},{"key":"e_1_2_2_31_1","volume-title":"IMPACT 2017 : 7th International Workshop on Polyhedral Compilation Techniques. https:\/\/hal.inria.fr\/hal-01505764","author":"Razanajato Harenome","year":"2017","unstructured":"Harenome Razanajato , Vincent Loechner , and C\u00e9dric Bastoul . 2017 . Splitting Polyhedra to Generate More Eficient Code . In IMPACT 2017 : 7th International Workshop on Polyhedral Compilation Techniques. https:\/\/hal.inria.fr\/hal-01505764 Harenome Razanajato, Vincent Loechner, and C\u00e9dric Bastoul. 2017. Splitting Polyhedra to Generate More Eficient Code. In IMPACT 2017 : 7th International Workshop on Polyhedral Compilation Techniques. https:\/\/hal.inria.fr\/hal-01505764"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45231-8_41"},{"volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","key":"e_1_2_2_33_1","unstructured":"Alexander Schrijver . 1998. Theory of Linear and Integer Programming . Wiley . Alexander Schrijver. 1998. Theory of Linear and Integer Programming. Wiley."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(1:10)2011"},{"volume-title":"GROW' 10 : 2nd GCC Research Opportunities Workshop. https:\/\/hal.inria.fr\/inria-00551516","author":"Trifunovi\u0107 Konrad","key":"e_1_2_2_36_1","unstructured":"Konrad Trifunovi\u0107 , Albert Cohen , David Edelsohn , Feng Li , Tobias Grosser , Harsha Jagasia , Razya Ladelsky , Sebastian Pop , Jan Sj\u00f6din , and Ramakrishna Upadrasta . 2010. GRAPHITE Two Years After: First Lessons Learned From Real-World Polyhedral Compilation . In GROW' 10 : 2nd GCC Research Opportunities Workshop. https:\/\/hal.inria.fr\/inria-00551516 Konrad Trifunovi\u0107, Albert Cohen, David Edelsohn, Feng Li, Tobias Grosser, Harsha Jagasia, Razya Ladelsky, Sebastian Pop, Jan Sj\u00f6din, and Ramakrishna Upadrasta. 2010. GRAPHITE Two Years After: First Lessons Learned From Real-World Polyhedral Compilation. In GROW' 10 : 2nd GCC Research Opportunities Workshop. https:\/\/hal.inria.fr\/inria-00551516"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706311"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3355606"},{"key":"e_1_2_2_40_1","volume-title":"Schedule Trees. In IMPACT 2014: 4th International Workshop on Polyhedral Compilation Techniques, Sanjay Rajopadhye and Sven Verdoolaege (Eds.). https:\/\/hal.inria.fr\/hal00911894","author":"Verdoolaege Sven","year":"2014","unstructured":"Sven Verdoolaege , Serge Guelton , Tobias Grosser , and Albert Cohen . 2014 . Schedule Trees. In IMPACT 2014: 4th International Workshop on Polyhedral Compilation Techniques, Sanjay Rajopadhye and Sven Verdoolaege (Eds.). https:\/\/hal.inria.fr\/hal00911894 Sven Verdoolaege, Serge Guelton, Tobias Grosser, and Albert Cohen. 2014. Schedule Trees. In IMPACT 2014: 4th International Workshop on Polyhedral Compilation Techniques, Sanjay Rajopadhye and Sven Verdoolaege (Eds.). https:\/\/hal.inria.fr\/hal00911894"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362390"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-3402-z"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434321","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434321","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:47Z","timestamp":1750195907000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434321"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434321"],"URL":"https:\/\/doi.org\/10.1145\/3434321","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}