2021/03/23 by Rongxiao Fu, Fu, Rongxiao, Xueying Qin +5 · 1 citation
Computer Science · #Compiler #Computer science #Correctness #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Program analysis #Program transformation #Programming Languages (cs.PL) #Programming language #Rewriting #Security and Verification in Computing #Type (biology) #cs.PL
paper · pdf · doi:10.48550/arxiv.2103.13390
published in arXiv (Cornell University) (Cornell University)
arxiv created 2021/03/23 · openalex publication_date 2021/03/23 · arxiv updated 2021/03/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non meaningful compositions of rewrites that otherwise would fail during rewriting at runtime. Furthermore, our type system enables reasoning about how rewriting transforms the shape of the computational program. We present a formalization of our language at its type system and demonstrate its practical use for expressing compiler optimization strategies. Our type system builds the foundation for many interesting future applications, including verifying the correctness of program transformations and synthesizing program transformations from specifications encoded as types.