Abstract
CASL is a specification language combining first-order logic, partiality and subsorting. This paper generalizes the CASL logic to also include higher-order functions and predicates. The logic is presented in a modular step-by-step reduction: the logic is defined in terms of a generalized subsorted partial logic which in turn is defined in terms of many-sorted partial first-order logic. A new notion of homomorphism is introduced to meet the need to get a faithful embedding of first-order CASL into higher-order CASL. Finally, it is discussed how a proof calculus for the proposed logic can be developed.
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.
Similar content being viewed by others
References
Adámek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories. Wiley, Chichester (1990)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic press, London (1986)
Astesiano, E., Cerioli, M.: On the existence of initial models for partial (higherorder) conditional specifications. In: Díaz, J., Orejas, F. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol. 351, pp. 74–88. Springer, Heidelberg (1989)
Astesiano, E., Cerioli, M.: Partial Higher–Order Specifications. Fundamenta Informaticae 16, 101–126 (1992)
Barendregt, H.P.: The Lambda Calculus. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1991) (revised edition)
Barendregt, H.P.: Lambda calculi with types. In: Gabbai Samson Abramski, D.M., Maiboum, T.S.E. (eds.) Handbook of Logic in Computer Science. Oxford University Press, Oxford (1992)
Borzyszkowski, T.: Moving specification structures between logical systems. Presented at the WADT 1998 workshop, Lisbon (1998)
Broy, M., Facchi, C., Grosu, R., Hettler, R., Hussmann, H., Nazareth, D., Regensburger, F., Stølen, K.: The requirement and design specification language Spectrum, an informal introduction, version 1.0. Technical report, Institut für Informatik, Technische Universität München (March 1993)
Burmeister, P.: A model theoretic approach to partial algebras. Akademie Verlag, Berlin (1986)
Cerioli, M., Meseguer, J.: May I borrow your logic (transporting logical structures along maps). Theoretical Computer Science 173, 311–347 (1997)
Cerioli, M., Mossakowski, T., Reichel, H.: From total equational to partial first order logic. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) Algebraic Foundations of Systems Specifications, pp. 31–104. Springer, Heidelberg (1999)
Cerioli, M., Haxthausen, A., Krieg-Brückner, B., Mossakowski, T.: Permissive subsorted partial logic in Casl. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 91–107. Springer, Heidelberg (1997)
Farmer, W.A.: A partial functions version of Church’s simple type theory. Journal of Symbolic Logic 55, 1269–1291 (1991)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39, 95–146 (1992); Predecessor in: LNCS, vol. 164, pp. 221–256 (1984)
Haxthausen, A.E.: Order-sorted algebraic specifications with higher-order functions. Theoretical Computer Science 183, 157–185 (1997)
Hoffmann, K., Ehrig, H., Wolter, U.: Folding and unfolding construction between algebraic high level nets and contextual higher order nets. Presented at WADT 1999 (1999)
Honsell, F., Sannella, D.: Pre-logical relations. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 546–561. Springer, Heidelberg (1999)
Kerber, M.: Sound and complete translations from sorted higher-order logic into sorted first-order logic. In: Wah, B.W., Georgeff, M., Shi, Z. (eds.) Proceedings of PRICAI 1994, Third Pacific Rim International Conference on Artificial Intelligence, pp. 149–154. International Academic Publishers, Beijing (1994)
Kohlhase, M.: Higher-order automated theorem proving. Unpublished draft, Universität Saarbücken (1999)
Krieg-Brückner, B., Sannella, D.: Structuring Specifications in-the-large and in-the-small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL. In: Abramsky, S., Maibaum, T.S.E. (eds.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 103–120. Springer, Heidelberg (1991)
CoFI Task Group on Language Design. Casl – The CoFI Algebraic Specification Language – Summary, version 1.0 (October 1998), Available at WWW, http://www.brics.dk/Projects/CoFI/Documents/CASLSummary/index.html
Martí-Oliet, N., Meseguer, J.: Inclusions and subtypes I: First-order case. Journal of Logic and Computation 6(3), 409–438 (1996)
Meinke, K.: Universal algebra in higher types. Theoretical Computer Science 100(2), 385–417 (1992)
Meseguer, J.: General logics. In: Logic Colloquium 87, pp. 275–329. North Holland, Amsterdam (1989)
Mossakowski, T., Kolyang, Krieg-Brückner, B.: Static semantic analysis and theorem proving for CASL. In: Parisi Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 333–348. Springer, Heidelberg (1998)
Mossakowski, T., Haxthausen, A., Krieg-Brückner, B.: Subsorted partial higher-order logic as an extension of casl. CoFI Note: L-10 (October 1998), Available at http://www.brics.dk/Projects/CoFI/Notes/L-10.html
Mosses, P.D.: CoFI: The Common Framework Initiative for Algebraic Specification and Development. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 115–137. Springer, Heidelberg (1997)
Poigné, A.: On specifications, theories, and models with higher types. Information and Control 68(1–3), 1–46 (1986)
Qian, Z.: An algebraic semantics of higher-order types with subtypes. Acta Informatica 30(6), 569–607 (1993)
Sannella, D.T., Burstall, R.M.: Structured theories in LCF. In: Ausiello, G., Protasi, M. (eds.) CAAP 1983. LNCS, vol. 159, pp. 377–391. Springer, Heidelberg (1983)
Schobbens, P.Y.: Second-order proof systems for algebraic specification languages. In: Ehrig, H., Orejas, F. (eds.) Abstract Data Types 1992 and COMPASS 1992. LNCS, vol. 785, pp. 321–336. Springer, Heidelberg (1994)
CoFI Task Group on Semantics. Casl – The CoFI Algebraic Specification Language (version 1.0) – Semantics. Version 0.95. CoFI Note: S-9 (March 1999), Available at http://www.brics.dk/Projects/CoFI/Notes/S-9.html
Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Owe, O., Dahl, O.-J. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)
Tarlecki, A.: Towards heterogeneous specifications. In: Gabbay, D., van Rijke, M. (eds.) Frontiers of Combining Systems, 2nd International Workshop. Kluwer, Dordrecht (1998) (to appear)
Tarlecki, A., Möller, B., Wirsing, M.: Algebraic specifications of reachable higherorder algebras. In: Sannella, D., Tarlecki, A. (eds.) Abstract Data Types 1987. LNCS, vol. 332, pp. 154–169. Springer, Heidelberg (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mossakowski, T., Haxthausen, A., Krieg-Brückner, B. (2000). Subsorted Partial Higher-Order Logic as an Extension of CASL. In: Bert, D., Choppy, C., Mosses, P.D. (eds) Recent Trends in Algebraic Development Techniques. WADT 1999. Lecture Notes in Computer Science, vol 1827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-44616-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-44616-3_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67898-4
Online ISBN: 978-3-540-44616-3
eBook Packages: Springer Book Archive