Abstract
In this paper we present the higher-order logic used in theorem-provers like the HOL system (see [GM 93]) or Isabelle HOL logic (see [Paul 94]) as an institution. Then we show that for maps of institutions into HOL that satisfy certain technical conditions we can reuse the proof system of the higher-order logic to reason about structured specifications built over the institutions mapped into HOL. We also show some maps of institutions underlying the CASL specification formalism (see [CASL 99]) into HOL that satisfy conditions needed for reusing proof systems.
This research was partially supported by ESPRIT CRIT2 program, working group 29432 (CoFI WG) and KBN grant 8 T11C 037 16.
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
Andrews, P.B.: An introduction to mathematical logic and type theory: to truth through proof. Academic Press, INC., London (1986)
Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics. Studies in Logic and The Foundations of Mathematics. Elsevier, Amsterdam (1998)
Borzyszkowski, T.: Moving specification structures between logical systems. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol. 1589, pp. 16–28. Springer, Heidelberg (1998)
Borzyszkowski, T.: Logical systems for structured specifications. Special issue of Theoretical Computer Science (to appear), See http://monika.univ.gda.pl/~mattb/papers.html
CASL The Common Algebraic Specification Language - Summary, by The CoFI Task Group on Language Design. Version 1.0 (March 19, 1999), Document is available on http://www.brics.dk/Projects/CoFI/Notes/S-9/ and ftp://ftp.brics.dk/Projects/CoFI/Notes/S-9/
Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Undergraduate Texts in Mathematics. Springer, Heidelberg (1996)
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specifications and programming. Journal of the Assoc. for Computing Machinery 39, 95–146 (1992)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)
Meseguer, J.: General logic. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium 1987, pp. 279–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, Springer, Heidelberg (1998)
Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Sannella, D., SokoGlowski, S., Tarlecki, A.: Towards formal development of programs from algebraic specification: parameterization revisited. Acta Informatica 29, 689–736 (1992)
Tarlecki, A.: Moving between logical systems. Recent Trends in Data Type Specifications. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)
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
Borzyszkowski, T. (2000). Higher-Order Logic and Theorem Proving for Structured Specifications. 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_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-44616-3_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67898-4
Online ISBN: 978-3-540-44616-3
eBook Packages: Springer Book Archive