Formalising Monotone Frameworks: A dependently typed implementation in Agda
Summary
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.