Abstract
This paper is based on previous work by Harper, Sannella and Tarlecki who suggest a framework for giving semantic interpretations to logic representations in the LF logical framework. Besides LF, there are also other approaches that tackle the representation of logics in a meta-logic. The logic-independent aspect in the formal development of software has been investigated intensively based on abstract model theory. Less attention is paid to the proof system aspect. In this paper we treat logic-independence by considering the consequence relation that models a proof system for a logic. The existing work is generalized here to the consideration of any logic as a meta-logic, since there may be meta-logics other than LF that are more suitable and convenient for developing “object” logical systems. This generalized framework is then used for building logic-independent specifications and developments. The setting can eventually be considered as a firm semantic basis for developing logic-independent transformations.
This work is partially supported by the German Ministry of Research and Technology (BMFT) as part of the project “KORSO — Korrekte Software”
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
M. Arbib, E. Manes. Arrows, Structures, and Functors-the Categorical Imperative. New York, London: Academic Press 1975.
H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification I: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science New York: Springer (1985).
H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification II. EATCS Monographs on Theoretical Computer Science New York: Springer (1990).
P. Gardner. Representing Logics in Type Theory. Phd Thesis, LFCS Report ECS-LFCS-92-227, Dept. of Computer Science, Uni. of Edinburgh.
J.A. Goguen, R.M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. J. ACM, vol. 39, No. 1, pp 95–146 (Jan. 1992).
R. Harper, F. Honsell, G. Plotkin. A Framework for Defining Logics. Proc. 2nd IEEE Symp. on Logic in Computer Science, Conell, pp 194–204 (1987).
R. Harper, D. Sannella, A. Tarlecki. Structure and Representation in LF. LFCS Report ECS-LFCS-89-75, Dept. of Computer Science, Uni. of Edinburgh.
R. Harper, D. Sannella, A. Tarlecki. Logic Representation in LF. Proc. 3nd Summer Conference in Category Theory and Computer Science, LNCS 389, pp 250–272 (1989).
B. Krieg-Brückner, D. Sannella. Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL. Proc. TAPSOFT 91, LNCS 582(1991).
B. Krieg-Brückner, E. Karlsen, J. Liu, O. Traynor. The PROSPECTRA Methodology and System: Uniform Transformational (Meta-) Development. VDM '91: Formal Software Development Methods, S. Prchn W.J. Toctenel (eds.), LNCS 552, pp 362–397.
B. Hoffmann, B. Krieg-Brückner (eds.): PROgram development by SPECification and TRAnsformation: Methodology, Language Family, System. LNCS 680 (1993).
J. Lambek, P.J. Scott. Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics 7, Cambridge University Press 1986.
Z. Luo. An Extended Calculus of Constructions. Phd Thesis, LFCS Report ECS-LFCS-90-118, Dept. of Computer Science, Uni. of Edinburgh.
J. Meseguer. General Logics, Proc. of the Logic Colloquium '87, H. D. Ebbinghaus et al. (eds.), North Holland.
F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. Plotkin (eds.): Logical Frameworks. Cambridge University Press 1991.
D. Sannella, S. Sokolowski, A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterization revisited. Report 6/90, Informatik, Universität Bremen (1990).
D. Sannella, A. Tarlecki. Towards formal development of programs from algebraic specifications: implementations revisited. In H. Ehrig et al.(eds.): TAPSOFT 87 LNCS 249 pp 96–110 (1987).
D. Sannella, M. Wirsing. A kernel language for algebraic specifications and implementations LNCS 158, pp 413–427 (1983).
L. Paulson. The foundations of a generic theorem prover. Technical Report 130, Computer Laboratory, University of Cambridge.
L. Paulson. Logics and Computation: interactive proof with Cambridge LCF. Cambridge Tracts in Theoretical Computer Science 2, Cambridge University Press 1987.
M. Wirsing. Structured Algebraic Specifications: a kernel language. TCS 42, pp 123–249 (1986).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, J. (1994). A semantic basis for logic-independent transformation. In: Ehrig, H., Orejas, F. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1992 1992. Lecture Notes in Computer Science, vol 785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57867-6_16
Download citation
DOI: https://doi.org/10.1007/3-540-57867-6_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57867-3
Online ISBN: 978-3-540-48361-8
eBook Packages: Springer Book Archive