Extended ML: An institution-independent framework for formal program development

Donald Sannella, Andrzej Tarlecki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationCategory Theory and Computer Programming
Subtitle of host publicationTutorial and Workshop, Guildford, U.K. September 16–20, 1985 Proceedings
EditorsDavid Pitt, Samson Abramsky, Axel Poigné, David Rydeheard
PublisherSpringer Berlin Heidelberg
Pages364-389
Number of pages26
ISBN (Electronic)978-3-540-47213-1
ISBN (Print)978-3-540-17162-1
DOIs
Publication statusPublished - 1986

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume240
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Extended ML: An institution-independent framework for formal program development'. Together they form a unique fingerprint.

Cite this