Formalize a realistic language

To gain confidence in the axioms we use for abstracting away the language, and in our lifting lemmas, it'd be great if we could have a formalization of the lambda-calculus we used in the paper (or maybe one with a heap, I don't care strongly either way).

@swasey I think you're the one who did most work in this direction.