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:

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

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

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.


Written 3 May 1995.