Abstract
The notion of data type specification refinement is discussed in a setting of System F and the logic for parametric polymorphism of Plotkin and Abadi. At first order, one gets a notion of specification refinement up to observational equivalence in the logic simply by using Luo’s formalism. This paper generalises this notion to abstract data types whose signatures contain higher-order and polymorphic functions. At higher order, the tight connection in the logic between the existence of a simulation relation and observational equivalence ostensibly breaks down. We show that an alternative notion of simulation relation is suitable. This also gives a simulation relation in the logic that composes at higher order, thus giving a syntactic logical counterpart to recent advances on the semantic level.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. Theoretical Computer Science, 121:9–58, 1993.
D. Aspinall. Type Systems for Modular Programs and Specifications. PhD thesis, University of Edinburgh, 1998.
E.S. Bainbridge, P.J. Freyd, A. Scedrov, and P.J. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35–64, 1990.
M. Bidoit and R. Hennicker. Behavioural theories and the proof of behavioural properties. Theoretical Computer Science, 165:3–55, 1996.
M. Bidoit, R. Hennicker, and M. Wirsing. Behavioural and abstractor specifications. Science of Computer Programming, 25:149–186, 1995.
M. Bidoit, R. Hennicker, and M. Wirsing. Proof systems for structured specifications with observability operators. Theoretical Computer Sci., 173:393–443, 1997.
C. Böhm and A. Beraducci. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science, 39:135–154, 1985.
V. Breazu-Tannen and T. Coquand. Extensional models for polymorphism. Theoretical Computer Science, 59:85–114, 1988.
M. Cerioli, M. Gogolla, H. Kirchner, B. Krieg-Brückner, Z. Qian, and M. Wolf. Algebraic System Specification and Development. Survey and Annotated Bibliography, 2nd Ed., volume 3 of Monographs of the Bremen Institute of Safe Systems. Shaker, 1997. 1st edition available in LNCS 501, Springer, 1991.
J.A. Goguen. Parameterized programming. IEEE Transactions on Software Engineering, SE-10(5):528–543, 1984.
J.A. Goguen and R. Burstall. CAT, a system for the structured elaboration of correct programs from structured specifications. Tech. Rep. CSL-118, SRI International, 1980.
J.E. Hannay. Specification refinement with System F. In Proc. CSL’99, volume 1683 of LNCS, pages 530–545, 1999.
J.E. Hannay. Specification refinement with System F, the higher-order case. Submitted for publication, 2000.
R. Hasegawa. Parametricity of extensionally collapsed term models of polymorphism and their categorical properties. In Proc. TACS’91, volume 526 of LNCS, pages 495–512, 1991.
R. Hennicker. Structured specifications with behavioural operators: Semantics, proof methods and applications. Habilitationsschrift, LMU, München, 1997.
C.A.R. Hoare. Proofs of correctness of data representations. Acta Inform., 1:271–281, 1972.
F. Honsell, J. Longley, D. Sannella, and A. Tarlecki. Constructive data refinement in typed lambda calculus. In Proc. FOSSACS 2000, LNCS, 2000.
F. Honsell and D. Sannella. Pre-logical relations. In Proc. CSL’99, volume 1683 of LNCS, pages 546–561, 1999.
A. Jung and J. Tiuryn. A new characterization of lambda definability. In Proc. of TLCA 93, volume 664 of LNCS, pages 245–257, 1993.
Y. Kinoshita, P.W. O’Hearn, A.J. Power, M. Takeyama, and R.D. Tennent. An axiomatic approach to binary logical relations with applications to data refinement. In Proc. of TACS’97, volume 1281 of LNCS, pages 191–212, 1997.
Y. Kinoshita and A.J. Power. Data refinement for call-by-value programming languages. In Proc. CSL’99, volume 1683 of LNCS, pages 562–576, 1999.
Z. Luo. Program specification and data type refinement in type theory. Math. Struct. in Comp. Sci., 3:333–363, 1993.
Q. Ma and J.C. Reynolds. Types, abstraction and parametric polymorphism, part 2. In Proc. 7th MFPS, volume 598 of LNCS, pages 1–40, 1991.
H. Mairson. Outline of a proof theory of parametricity. In ACM Symposium on Functional Programming and Computer Architecture, volume 523 of LNCS, pages 313–327, 1991.
J.C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305–330. Academic Press, 1991.
J.C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
J.C. Mitchell and G.D. Plotkin. Abstract types have existential type. ACM Trans. on Programming Languages and Systems, 10(3):470–502, 1988.
N. Mylonakis. Behavioural specifications in type theory. In Recent Trends in Data Type Spec., 11th WADT, volume 1130 of LNCS, pages 394–408, 1995.
A.M. Pitts. Parametric polymorphism and operational equivalence. In Proc. 2nd Workshop on Higher Order Operational Techniques in Semantics, volume 10 of ENTCS. Elsevier, 1997.
A.M. Pitts. Existential types: Logical relations and operational equivalence. In Proc. ICALP’98, volume 1443 of LNCS, pages 309–326, 1998.
G. Plotkin and M. Abadi. A logic for parametric polymorphism. In Proc. of TLCA 93, volume 664 of LNCS, pages 361–375, 1993.
G.D. Plotkin, A.J. Power, and D. Sannella. A compositional generalisation of logical relations. Submitted for publication, 2000.
E. Poll and J. Zwanenburg. A logic for abstract data types as existential types. In Proc. TLCA’99, volume 1581 of LNCS, pages 310–324, 1999.
B. Reus and T. Streicher. Verifying properties of module construction in type theory. In Proc. MFCS’93, volume 711 of LNCS, pages 660–670, 1993.
J.C. Reynolds. Types, abstraction and parametric polymorphism. Information Processing, 83:513–523, 1983.
D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150–178, 1987.
D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Inform., 25(3):233–281, 1988.
D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, 9:229–269, 1997.
O. Schoett. Data Abstraction and the Correctness of Modular Programming. PhD thesis, University of Edinburgh, 1986.
T. Streicher and M. Wirsing. Dependent types considered necessary for specification languages. In Recent Trends in Data Type Spec., volume 534 of LNCS, pages 323–339, 1990.
J. Underwood. Typing abstract data types. In Recent Trends in Data Type Spec., Proc. 10th WADT, volume 906 of LNCS, pages 437–452, 1994.
J. Zwanenburg. Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow. PhD thesis, Technische Universiteit Eindhoven, 1999.
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
Hannay, J.E. (2000). A Higher-Order Simulation Relation for System F. In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_9
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive