Abstract
We introduce an algebraic framework for the equational specification of algebras of types and combinators. A categorical semantics for type specifications is given based on cofibrations of categories of algebras. It is shown that each equational type specification admits an initial model semantics, and we present complete inference systems for type assignments and equations.
It is a pleasure to thank J.R. Hindley, J.V. Tucker and E.G. Wagner for helpful comments on this work. We also acknowledge the financial support of the Science and Engineering Research Council, the Nuffield Foundation and IBM T.J. Watson Research Center.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Barr and C. Wells, Category Theory for Computing Science, Prentice Hall, Englewood Cliffs, 1990.
H.B. Curry and R. Feys, Combinatory Logic, Vol. I, North Holland, Amsterdam, 1958.
H.B. Curry, J.R. Hindley and J.P. Seldin, Combinatory Logic, Vol. II, North Holland, Amsterdam, 1972.
J-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press, Cambridge, 1989.
J.R. Hindley and J.P. Seldin, Introduction to Combinators and λ-Calculus, Cambridge University Press, Cambridge, 1986.
K. Meinke, Universal algebra in higher types, Report CSR 12-90, Dept. of Computer Science, University College Swansea, to appear in Theoretical Computer Science, Volume 99, 1990.
K. Meinke, Subdirect representation of higher type algebras, to appear in K. Meinke and J.V. Tucker (eds), Many-Sorted Logic and its Applications, John Wiley, 1992.
K. Meinke, A recursive second order initial algebra specification of primitive recursion, Report CSR 8-91, Department of Computer Science, University College of Swansea,1991.
K. Meinke and J.V. Tucker, Universal algebra, to appear in: S. Abramsky, D. Gabbay and T.S.E. Maibaum, (eds) Handbook of Logic in Computer Science, Oxford University Press, Oxford, 1992.
K. Meinke and E. Wagner, Algebraic specification of types and combinators, IBM research report, in preparation, 1992.
J.C. Mitchell, Type systems for programming languages, in: J. van Leeuwen (ed), Handbook of Theoretical Computer Science, Volume B, Elsevier, Amsterdam, 1990.
B. Möller, Higher-order algebraic specifications, Facultät für Mathematik und Informatik, Technische Universität München, Habilitationsschrift, 1987b.
M. Nivat, J. Reynolds (eds), Algebraic Methods in Semantics, Cambridge University Press, Cambridge, 1985.
A. Poigné, On specifications, theories and models with higher types, Information and Control 68, (1986) 1–46.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meinke, K. (1992). Equational specification of abstract types and combinators. In: Börger, E., Jäger, G., Kleine Büning, H., Richter, M.M. (eds) Computer Science Logic. CSL 1991. Lecture Notes in Computer Science, vol 626. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023772
Download citation
DOI: https://doi.org/10.1007/BFb0023772
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55789-0
Online ISBN: 978-3-540-47285-8
eBook Packages: Springer Book Archive