Formalising Monotone Frameworks: A dependently typed implementation in Agda
Wijk, J.J. van
MetadataShow full item record
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.