Frédéric Besson, Thomas P. Jensen, David Pichardie: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364(3): 273-291 (2006)