Formalising Monotone Frameworks: A dependently typed implementation in Agda

Abstract

Compiler builders use monotone frameworks to perform static analysis. Often, they omit proof of the domain of the function being a bounded semi lattice or only argue why their domain should be. Unfortunately, mistakes in their argumentation could result in a non terminat- ing static analysis. Since important software, such as compilers, often depends on the results of a static analysis, embedding a non terminating analysis causes such software to loop. To assist programmers in their reasoning and to obtain machine verified proofs of termination, this thesis presents a verified implementation of embellished, ex- tended and regular monotone frameworks in Agda. The implementation contains several algorithms to compute the least fixed point of a function that represents the flow of information for the static analysis on an input program. That program is written in a simplified procedural programming language. To facilitate construction of termination proofs, we introduce a set of bounded semi lattice combinators which can be used to compose the domain of a transfer function. The bounded semi lattice constructed by the combinators includes a proof that the partial order is conversely well founded and thus implies the ascending chain condition. Finally, we perform classical analyses on a intra-procedural and inter-procedural language.