KIT | KIT-Bibliothek | Impressum | Datenschutz

Formally proving a compiler transformation safe

Breitner, Joachim

We prove that the Call Arity analysis and transformation, as implemented in the Haskell compiler GHC, is safe, i.e. does not impede the performance of the program. We formalized syntax, semantics, the analysis and the transformation in the interactive theorem prover Isabelle to obtain a machine-checked proof and hence a level of rigor rarely obtained for compiler optimization safety theorems. The proof is modular and introduces trace trees as a suitable abstraction in abstract cardinality analyses. We discuss the breadth of the formalization gap.

DOI: 10.1145/2804302.2804312
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2015
Sprache Englisch
Identifikator ISBN: 978-1-4503-3808-0
KITopen-ID: 1000049755
Erschienen in Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Vancouver, BC, Canada, September 01 - 03, 2015 . Ed.: B. Lippmeier
Verlag ACM, New York (NY)
Seiten 35-46
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page