kirancodes.me
To Proof Maintenance & Beyond!

Deriving Target Code as a Representation of Continuation Semantics

Mitchell Wand

Abstract

Reynolds' technique for deriving interpreters is extended to derive compilers from continuation semantics.The technique starts by eliminating h-variables from the semantic equations through the introduction of special-purpose combinators.The semantics of a program phrase may be represented by a term built from these combinators.Then associative and distributive laws are used to simplify the terms.Last, a machine is built to interpret the simplified terms as the functions they represent.The combinators reappear as the instructions of this machine.The technique is illustrated with three examples.

Related papers