WG211/M12Mosses

Component-Based Semantics for Caml Light by Peter Mosses (joint work with Martin Churchill)

We are exploring scalability of component-based programming language semantics via case studies. In particular, we translate Caml Light to language-independent fundamental constructs (funcons), each of which has independent semantics given by inductive rules. This factorisation provides an accessible semantic specification of the language, while retaining formal precision. The semantics can be validated by animating the translation and rules, and running test programs. Moreover, funcon equivalence laws (bisimulations) can be proved and used to deduce equivalence of programs; a recently developed rule format ensures that this is a congruence for all of our funcons. The funcons used form a basis of a growing repository to be used in further language specifications. This work forms part of the PLanCompS project