Types, Subtypes, and ASL+

ASL+ is a formalism for speci cation and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and re nement of speci cations, which can be seen as a type theory with subtyping, including contravariant re nement tracted speci cations and a notion of strati ed equality for higher-order objects. We describe the syntax of the language and a partial equivalence relation semantics. This style of semantics is familiar from subtyping calculi, but a novelty here is the use of a hierarchy of typed domains instead of a single untyped domain. We introduce the formal system for proving satisfaction and re nement and describe how it is linked to proof systems of the underlying programming and speci cation languages.

• Type: Conference
• Year: 1994
• Where: COMPASS
• Authors: David Aspinall
• Keywords: COMPASS 1994, Equivalence Relation Semantics, Programming Languages, Speci Cation, Strati Ed Equality