Abstracting Definitional Interpreters in lean

Stream: Program verification

[ohhaimark]

I've been trying to find a nice PLT orientated approach to static analysis and abstract interpretation. I found this functional pearl paper Abstracting Definitional Interpreters. I'm very much a noob, but the idea of getting an abstract interpreter from a definitional interpreter appeals to me, however with my limited knowledge this seems very much to be a toy.

The one of the papers it references (Abstracting Abstract Machines), stores continuations in an abstract heap, but this ability seems to be lost in the definitional approach as it uses the meta language's stack.

I was wondering if I could use lean meta programming / macros to write straightforward definitional interpreter, but generate and use a type for the continuations of a abstract machine underneath?