Seminars and other Research Lectures Seminars and other Research Lectures Abstract Interpretations for Free.
Abstract interpretation is a technique for safely approximating the behaviour of computer programs.
It is used widely in compiler optimisation and, increasingly, as a basis for model checking. We introduce the use of Galois connections in abstract interpretations and we show how given base Galois connections can be extended to Galois connections of arbitrary type. Generic programs are programs that are parameterised by one or more type constructors. Unlike their non-generic instances, the generic notions are not equivalent. The talk focuses on the notion of F-reductivity, a generic notion of program termination, emphasising its importance in the construction of recursive programs and discussing its basic properties.