2026-07-22T11:56:50Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12337 2024-03-06T10:50:00Z ddc:004 open_access

Data-Flow Analyses as Effects and Graded Monads Ivašković, Andrej Mycroft, Alan Orchard, Dominic data-flow analysis effect systems graded monads correctness 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrej Ivašković and Alan Mycroft and Dominic Orchard 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.15 urn:nbn:de:0030-drops-123376 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.15 eng https://creativecommons.org/licenses/by/3.0/legalcode