Types, subtypes, and ASL+

David Aspinall

doi:10.1007/BFb0014424

Types, subtypes, and ASL+

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

ASL+ is a formalism for specification and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and refinement of specifications, which can be seen as a type theory with subtyping, including contravariant refinement for II-abstracted specifications and a notion of stratified 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 refinement and describe how it is linked to proof systems of the underlying programming and specification languages.

Original language	English
Title of host publication	Recent Trends in Data Type Specification
Subtitle of host publication	10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers
Editors	Egidio Astesiano, Gianna Reggio, Andrzej Tarlecki
Publisher	Springer
Pages	116-131
Number of pages	16
Volume	906
ISBN (Electronic)	978-3-540-49198-9
ISBN (Print)	978-3-540-59132-0
DOIs	https://doi.org/10.1007/BFb0014424
Publication status	Published - 1995

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	906

Access to Document

10.1007/BFb0014424

http://dx.doi.org/10.1007/BFb0014424

Cite this

Aspinall, D. (1995). Types, subtypes, and ASL+. In E. Astesiano, G. Reggio, & A. Tarlecki (Eds.), Recent Trends in Data Type Specification: 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers (Vol. 906, pp. 116-131). (Lecture Notes in Computer Science; Vol. 906). Springer. https://doi.org/10.1007/BFb0014424

Aspinall, David. / Types, subtypes, and ASL+. Recent Trends in Data Type Specification: 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers. editor / Egidio Astesiano ; Gianna Reggio ; Andrzej Tarlecki. Vol. 906 Springer, 1995. pp. 116-131 (Lecture Notes in Computer Science).

@inproceedings{fb00145ce4d44e6b99ea4b36e051034b,

title = "Types, subtypes, and ASL+",

abstract = "ASL+ is a formalism for specification and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and refinement of specifications, which can be seen as a type theory with subtyping, including contravariant refinement for II-abstracted specifications and a notion of stratified 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 refinement and describe how it is linked to proof systems of the underlying programming and specification languages.",

author = "David Aspinall",

year = "1995",

doi = "10.1007/BFb0014424",

language = "English",

isbn = "978-3-540-59132-0",

volume = "906",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "116--131",

editor = "Egidio Astesiano and Gianna Reggio and Andrzej Tarlecki",

booktitle = "Recent Trends in Data Type Specification",

address = "United Kingdom",

}

Aspinall, D 1995, Types, subtypes, and ASL+. in E Astesiano, G Reggio & A Tarlecki (eds), Recent Trends in Data Type Specification: 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers. vol. 906, Lecture Notes in Computer Science, vol. 906, Springer, pp. 116-131. https://doi.org/10.1007/BFb0014424

Types, subtypes, and ASL+. / Aspinall, David.
Recent Trends in Data Type Specification: 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers. ed. / Egidio Astesiano; Gianna Reggio; Andrzej Tarlecki. Vol. 906 Springer, 1995. p. 116-131 (Lecture Notes in Computer Science; Vol. 906).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Types, subtypes, and ASL+

AU - Aspinall, David

PY - 1995

Y1 - 1995

N2 - ASL+ is a formalism for specification and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and refinement of specifications, which can be seen as a type theory with subtyping, including contravariant refinement for II-abstracted specifications and a notion of stratified 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 refinement and describe how it is linked to proof systems of the underlying programming and specification languages.

AB - ASL+ is a formalism for specification and programming in-the-large, based on an arbitrary institution. It has rules for proving the satisfaction and refinement of specifications, which can be seen as a type theory with subtyping, including contravariant refinement for II-abstracted specifications and a notion of stratified 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 refinement and describe how it is linked to proof systems of the underlying programming and specification languages.

U2 - 10.1007/BFb0014424

DO - 10.1007/BFb0014424

M3 - Conference contribution

SN - 978-3-540-59132-0

VL - 906

T3 - Lecture Notes in Computer Science

SP - 116

EP - 131

BT - Recent Trends in Data Type Specification

A2 - Astesiano, Egidio

A2 - Reggio, Gianna

A2 - Tarlecki, Andrzej

PB - Springer

ER -

Aspinall D. Types, subtypes, and ASL+. In Astesiano E, Reggio G, Tarlecki A, editors, Recent Trends in Data Type Specification: 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers. Vol. 906. Springer. 1995. p. 116-131. (Lecture Notes in Computer Science). doi: 10.1007/BFb0014424

Types, subtypes, and ASL+

Abstract

Publication series

Access to Document

Fingerprint

Cite this