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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Adámek, H. Herrlich, and G. E. Strecker, Abstract and concrete categories, Wiley Interscience, 1990.
D. Aspinall, Type systems for modular programming and specification, Ph.D. thesis, Edinburgh, 1997.
E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Brückner, P. D. Mosses, D. Sannella, and A. Tarlecki, Casl: the Common Algebraic Specification Language, Theoret. Comput. Sci. (2003), to appear.
E. Astesiano and M. Cerioli, Free objects and equational deduction for partial conditional specifications, Theoret. Comput. Sci. 152 (1995), 91–138.
S. Autexier and T. Mossakowski, Integrating HOL-Casl into the development graph manager Maya, Frontiers of Combining Systems, LNCS, vol. 2309, Springer, 2002, pp. 2–17.
G. Berry and P.-L. Curien, Sequential algorithms on concrete data structures, Theoret. Comput. Sci. 20 (1982), 265–321.
V. Breazu-Tannen and A. R. Meyer, Lambda calculus with constrained types, Logic of Programs, LNCS, vol. 193, Springer, 1985, pp. 23–40.
CoFI, The Common Framework Initiative for algebraic specification and development, electronic archives, http://www.brics.dk/Projects/CoFI.
CoFI Language Design Task Group, Casl—The CoFI Algebraic Specification Language—Summary, version 1.0, Document/CASL/Summary, in [8], July 1999.
CoFI Semantics Task Group, Casl—The CoFI Algebraic Specification Language—Semantics, Note S-9 (version 0.96), in [8], July 1999.
T. Coquand, An analysis of Girard’s paradox, Logic in Computer Science, IEEE, 1986, pp. 227–236.
J. Goguen, A categorical manifesto, Math. Struct. Comput. Sci. 1 (1991), 49–67.
R. Grosu and F. Regensburger, The semantics of spectrum, LNCS 816 (1994), 124–145.
J. V. Guttag, J. J. Horning, S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing, Larch: Languages and tools for formal specification, Springer, 1993.
L. Henkin, The completeness of the first-order functional calculus, J. Symbolic Logic 14 (1949), 159–166.
J. M. E. Hyland, First steps in synthetic domain theory, Category Theory, LNM, vol. 1144, Springer, 1992, pp. 131–156.
S. Kahrs, D. Sannella, and A. Tarlecki, The definition of extended ML: A gentle introduction, Theoret. Comput. Sci. 173 (1997), 445–484.
J. Lambek and P. J. Scott, Introduction to higher-order categorical logic, Cambridge, 1986.
S. Mac Lane, Categories for the working mathematician, Springer, 1997.
J. C. Mitchell and P. J. Scott, Typed lambda models and cartesian closed categories, Categories in Computer Science and Logic, Contemp. Math., vol. 92, Amer. Math. Soc., 1989, pp. 301–316.
E. Moggi, Categories of partial morphisms and the λ p -calculus, Category Theory and Computer Programming, LNCS, vol. 240, Springer, 1986, pp. 242–251.
E. Moggi, The partial lambda calculus, Ph.D. thesis, University of Edinburgh, 1988.
T. Mossakowski, A. Haxthausen, and B. Krieg-Brückner, Subsorted partial higherorder logic as an extension of Casl, Workshop on Abstract Datatypes, LNCS, vol. 1827, Springer, 2000, pp. 126–145.
Till Mossakowski, Casl: From semantics to tools, Tools and Algorithms for Construction and Analysis of Systems, LNCS, vol. 1785, Springer, 2000, pp. 93–108.
G. Plotkin, Domains (the ‘Pisa Notes’), http://www.dcs.ed.ac.uk/home/gdp/
A. Poigné, On specifications, theories, and models with higher types, Inform. and Control 68 (1986), no. 1–3, 1–46.
F. Regensburger, HOLCF: Higher order logic of computable functions, Theorem Proving in Higher Order Logics, LNCS, vol. 971, 1995, pp. 293–307.
L. Schröder, Classifying categories for partial equational logic, Category Theory and Computer Science, ENTCS, 2002, to appear.
L. Schröder and T. Mossakowski, The definition ofHasCasl, in preparation.
D. S. Scott, Relating theories of the λ-calculus, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms, Academic Press, 1980, pp. 403–450.
M. Wenzel, Type classes and overloading in higher-order logic, Theorem Proving in Higher Order Logics, LNCS, vol. 1275, Springer, 1997, pp. 307–322.
Glynn Winskel, The formal semantics of programming languages, MIT, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schröder, L., Mossakowski, T. (2002). HasCasl: Towards Integrated Specification and Development of Functional Programs. In: Kirchner, H., Ringeissen, C. (eds) Algebraic Methodology and Software Technology. AMAST 2002. Lecture Notes in Computer Science, vol 2422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45719-4_8
Download citation
DOI: https://doi.org/10.1007/3-540-45719-4_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44144-1
Online ISBN: 978-3-540-45719-0
eBook Packages: Springer Book Archive