by Lutz Schröder and Till Mossakowski
Abstract:
The development of programs in modern functional languages such as Haskell calls for a wide-spectrum specification formalism that supports the type system of such languages, in particular higher order types, type constructors, and parametric polymorphism, and that contains a functional language as an executable subset in order to facilitate rapid prototyping. We lay out the design of HasCASL, a higher order extension of the algebraic specification language CASL that is geared towards precisely this purpose. Its semantics is tuned to allow program development by specification refinement, while at the same time staying close to the set-theoretic semantics of first order CASL. The number of primitive concepts in the logic has been kept as small as possible; we demonstrate how various extensions to the logic, in particular general recursion, can be formulated within the language itself.
Reference:
Lutz Schröder and Till Mossakowski: HasCASL: towards integrated specification and development of functional programs, In Hélène Kirchner, Christophe Ringeissen, eds.: Algebraic Methodology And Software Technology (AMAST 2002), Lecture Notes in Computer Science, vol. 2422, pp. 99–116, Springer; Berlin; http://www.springer.de, 2002. [preprint]
Bibtex Entry:
@InProceedings{SchroderMossakowski02,
author = {Lutz Schr{\"o}der and Till Mossakowski},
title = {{HasCASL}: towards integrated specification and development of functional programs},
year = {2002},
editor = {H{\'e}l{\`e}ne Kirchner and Christophe Ringeissen},
booktitle = {Algebraic Methodology And Software Technology (AMAST 2002)},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {2422},
pages = {99--116},
keywords = {CASL HasCASL general recursion functional programming partial lambda-calculus},
url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2755&spage=425},
comment = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/papers/recursion.ps">[preprint]</a>},
abstract = {The development of programs in modern functional languages such as Haskell calls for a wide-spectrum specification formalism that supports the type system of such languages, in particular higher order types, type constructors, and parametric polymorphism, and that contains a functional language as an executable subset in order to facilitate rapid prototyping. We lay out the design of HasCASL, a higher order extension of the algebraic specification language CASL that is geared towards precisely this purpose. Its semantics is tuned to allow program development by specification refinement, while at the same time staying close to the set-theoretic semantics of first order CASL. The number of primitive concepts in the logic has been kept as small as possible; we demonstrate how various extensions to the logic, in particular general recursion, can be formulated within the language itself.},
}