Abstract
The second-order lambda calculus allows an elegant formalisation of abstract data types (ADT’s) using existential types. Plotkin and Abadi’s logic for parametricity [PA93] then provides the useful proof principle of simulation for ADT’s, which can be used to show equivalence of data representations. However, we show that this logic is not sufficient for reasoning about specifications of ADT’s, and we present an extension of the logic that does provide the proof principles for ADT’s that we want.
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
H.P. Barendregt. Lambda calculi with types. In D.M. Gabbai, S. Abramsky, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1. Oxford University Press, 1992.
E.S. Bainbridge, P.J. Freyd, A. Scedrov, and P.J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35–64, 1990.
G. Barthe and J.H. Geuvers. Congruence types. In CSL’95, volume 1092 of Lecture Notes in Computer Science, pages 36–51. Springer, 1996.
R.L. Constable et al. Implementing Mathematics in the Nuprl proof development system. Prentice-Hall, 1986.
Thierry Coquand and Christine Paulin. Inductively Defined Types. In P. Martin-Löf and G. Mints, editors, COLOG-88, volume 417 of Lecture Notes in Computer Science, pages 50–66. Springer, 1990.
M. J. Gordon and T. F. Melham. Introduction to HOL. Cambridge, 1993.
Martin Hofmann. A simple model for quotient types. In TLCA’95, volume 902 of Lecture Notes in Computer Science, pages 216–234, 1995.
John C. Mitchell. On the equivalence of data representations. In Artificial Intelligence and Mathematical Theory of Computation, pages 305–330. Academic Press, 1991.
John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Trans. on Prog. Lang. and Syst., 10(3):470–502, 1988.
Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In TLCA’93, volume 664 of Lecture Notes in Computer Science, pages 361–375, 1993.
Christine Paulin-Mohring. Inductive definitions in the system Coq. In TLCA’93, volume 664 of Lecture Notes in Computer Science, pages 328–345. Springer, 1993.
Erik Poll. A Programming Logic based on Type Theory. PhD thesis, Technische Universiteit Eindhoven, 1994.
Izumi Takeuti. An axiomatic system of parametricity. In TLCA’97, volume 1130 of Lecture Notes in Computer Science, pages 354–372, 1997.
Jan Zwanenburg. The proof assistant Yarrow. Submitted for publication. See also http://www.win.tue.nl/cs/pa/janz/yarrow/, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poll, E., Zwanenburg, J. (1999). A Logic for Abstract Data Types as Existential Types. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_22
Download citation
DOI: https://doi.org/10.1007/3-540-48959-2_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65763-7
Online ISBN: 978-3-540-48959-7
eBook Packages: Springer Book Archive