Executing an SECD machine using logic programming

Abstract

Students usually find formal methods of describing programming languages very difficult because of the cryptic notation, the complexity of the techniques, and the size of the specifications. The SECD abstract machine provides a small but clear description of the operational semantics of the lambda calculus. By implementing the SECD machine in Prolog, we give students a tool for testing specifications and for experimenting with alternate language semantics in an interactive setting.