## Extended ML : An Institution-independent Framework for Formal
Program Development

**D. Sannella and A. Tarlecki**
*Abstract:* The Extended ML specification language provides
a framework for the formal stepwise development of modular programs
in the Standard ML programming language from specifications. The
object of this paper is to equip Extended ML with a semantics which
is completely independent of the logical system used to write
specifications, building on Goguen and Burstall's work on the
notion of an *institution* as a formalisation of the concept
of a logical system. One advantage of this is that it permits
freedom in the choice of the logic used in writing specifications;
an intriguing side-effect is that it enables Extended ML to be used
to develop programs in languages other than Standard ML since we
view programs as simply Extended ML specifications which happen to
include only ``executable'' axioms. The semantics of Extended ML is
defined in terms of the primitive specification-building operations
of the ASL kernel specification language which itself has an
institution-independent semantics.

It is not possible to give a semantics for Extended ML in an
institutional framework without extending the notion of an
institution; the new notion of an *institution with syntax* is
introduced to provide an adequate foundation for this enterprise.
An institution with syntax is an institution with three additions:
the category of signatures is assumed to form a concrete category;
an additional functor is provided which gives concrete syntactic
representations of sentences; and a natural transformation
associates these concrete objects with the ``abstract'' sentences
they represent. We use the first addition to ``lift'' certain
necessary set-theoretic constructions to the category of
signatures, and the other two additions to deal with the low-level
semantics of axioms.

*LFCS report
ECS-LFCS-86-16*

Previous |

Index |

Next