Types, Subtypes, and ASL+

12 years 9 months ago
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.
David Aspinall
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Authors David Aspinall
Comments (0)