Skip to content
Abstracting Definitional Interpreters
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

Abstracting Definitional Interpreters

Build Status


We show that a definitional interpreter written in monadic style can express not only the usual notion of interpretation, but also a wide variety of collecting semantics, abstract interpretations, symbolic execution, and their intermixings. We give a rational reconstruction of a definitional abstract interpreter for a higher-order language by building a series of components implementing monadic operations. The denouement of our story is a computable abstract interpreter that arises from the composition of simple, independent components. Remarkably, this interpreter implements a form of pushdown control flow analysis (PDCFA) in which calls and returns are always properly matched in the abstract semantics. True to the definitional style of Reynolds, the evaluator involves no explicit mechanics to achieve this property; it is simply inherited from the defining language.

For more, see:


This code has been tested with Racket 6.9, but probably works with other versions of Racket too.

To install:

   raco pkg install

To test:

   raco test --package abstracting-definitional-interpreters

This will test every module in the implementation. If no errors occur, the code is working as expected.

To uninstall:

   raco pkg remove abstracting-definitional-interpreters
You can’t perform that action at this time.