Bidirectional data-flow analyses, type-systematically

10 years 8 months ago
Bidirectional data-flow analyses, type-systematically
We show that a wide class of bidirectional data-flow analyses and program optimizations based on them admit declarative descriptions in the form of type systems. The salient feature is a clear separation between what constitutes a valid analysis and how the strongest one can be computed (via the type checking versus principal type inference distinction). The approach also facilitates elegant relational semantic soundness definitions and proofs for analyses and optimizations, with an application to mechanical transformation of program proofs, useful in proof-carrying code. Unidirectional forward and backward analyses are covered as special cases; the technicalities in the general bidirectional case arise from more subtle notions of valid and principal types. To demonstrate the viability of the approach we consider two examples that are inherently bidirectional: type inference (seen as a data-flow problem) for a structured language where the type of a variable may change over a progr...
Maria João Frade, Ando Saabas, Tarmo Uustal
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2009
Where PEPM
Authors Maria João Frade, Ando Saabas, Tarmo Uustalu
Comments (0)