Repository logo
 

Data-flow analyses as effects and graded monads

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Ivašković, A 
Orchard, D 

Abstract

In static analysis, two frameworks have been studied extensively: monotone data-flow analysis and type-and-effect systems. Whilst both are seen as general analysis frameworks, their relationship has remained unclear. Here we show that monotone data-flow analyses can be encoded as effect systems in a uniform way, via algebras of transfer functions. This helps to answer questions about the most appropriate structure for general effect algebras, especially with regards capturing control-flow precisely. Via the perspective of capturing data-flow analyses, we show the recent suggestion of using effect quantales is not general enough as it excludes non-distributive analyses e.g., constant propagation. By rephrasing the McCarthy transformation, we then model monotone data-flow effects via graded monads. This provides a model of data-flow analyses that can be used to reason about analysis correctness at the semantic level, and to embed data-flow analyses into type systems.

Description

Keywords

Journal Title

Leibniz International Proceedings in Informatics, LIPIcs

Conference Name

Formal Structures for Computation and Deduction

Journal ISSN

1868-8969

Volume Title

167

Publisher

Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Sponsorship
Trinity College, Cambridge (Internal Graduate Scholarship) EPSRC grant EP/T013516/1