Program Semantics in Miranda

This material explains the use of the functional programming language Miranda as a vehicle for describing the semantics of imperative programming languages. In particular we give a Miranda denotational description of a substantial subset of Pascal, describing a number of variants of the semantics, including parameter passing by value-result, dynamic binding of values to names and a simple semantics of jumps.

We also give an executable operational semantics of our basic language, as well as a compiler for this language into a simple stack machine, which is itself modelled in Miranda.

There is a paper available describing the material:

• Paper describing the Miranda material

The approach to explaining semantics which we have introduced here has a number of advantages.

• The semantics is presented in a familiar language. In presenting the operational semantics given in the paper I was surprised to find that students were happier with the Miranda description rather than the more abstract and less cluttered rule-based version,
• The semantics is type checked and executable, so we can validate it. It also allows us to prototype ideas in language design.

The Miranda libraries implementing the material can be found in the tar files below.

• semantics.tar.gz
• semantics.tar.Z

Please note that I erroneously put .x instead of .m files into the distributions here until 30 May. Please get new copies if necessary. Apologies for any problems caused!

To expand the tar file, type

tar xf semantics.tar

on your machine.

Up