Towards a Unifying Semantics Playground

By: Andrew Butterfield

Abstract

We give a brief presentation of how Unifying Theories of Programming (UTP) can be used to define program languages and their semantics. We describe and show examples of the use of a prototype theorem-prover reasonEq that supports equational reasoning for UTP. We discuss how this tool is intended to support work into various formal approaches to concurrency.

Keywords

Unifying Theories of Programming, Theory Prototyping, Formal Semantics

Cite as:

Andrew Butterfield, “Towards a Unifying Semantics Playground”, Journal of Object Technology, Volume 25, no. 1 ( 2026), pp. 1:1-13, doi:10.5381/jot.2026.25.1.a5.

DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn