Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Semantic and Syntactic Approaches to Simulation Relations

  • Conference paper
Mathematical Foundations of Computer Science 2003 (MFCS 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2747))

  • 1153 Accesses

Abstract

Simulation relations are tools for establishing the correctness of data refinement steps. In the simply-typed lambda calculus, logical relations are the standard choice for simulation relations, but they suffer from certain shortcomings; these are resolved by use of the weaker notion of pre-logical relations instead. Developed from a syntactic setting, abstraction barrier-observing simulation relations serve the same purpose, and also handle polymorphic operations. Meanwhile, second-order pre-logical relations directly generalise pre-logical relations to polymorphic lambda calculus (System F). We compile the main refinement-pertinent results of these various notions of simulation relation, and try to raise some issues for aiding their comparison and reconciliation.

This research was partly supported by the MRG project (IST-2001-33149) which is funded by the EC under the FET proactive initiative on Global Computing. SK was supported by an LFCS studentship.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Bainbridge, E., Freyd, P., Scedrov, A., Scott, P.: Functorial polymorphism. Theoretical Computer Science 70, 35–64 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bellucci, R., Abadi, M., Curien, P.-L.: A model for formal parametric polymorphism: a PER interpretation for system R. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 32–46. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  3. Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Science of Computer and Programming 25, 149–186 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  4. Böhm, C., Berarducci, A.: Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science 39, 135–154 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bruce, K., Meyer, A., Mitchell, J.: The semantics of the second-order lambda calculus. Information and Computation 85(1), 76–134 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  6. Girard, J.-Y.: Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: Proc. 2nd Scandinavian Logic Symp., Oslo. Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63–92. North-Holland, Amsterdam (1971)

    Chapter  Google Scholar 

  7. Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1990)

    Google Scholar 

  8. Hannay, J.: Specification refinement with System F. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 530–545. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Hannay, J.: A higher-order simulation relation for System F. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 130–145. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Hannay, J.: Abstraction Barriers and Refinement in the Polymorphic Lambda Calculus. PhD thesis, Laboratory for Foundations of Computer Science (LFCS), University of Edinburgh (2001)

    Google Scholar 

  11. Hannay, J.: Abstraction barrier-observing relational parametricity. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 135–152. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Hasegawa, R.: Parametricity of extensionally collapsed term models of polymorphism and their categorical properties. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 495–512. Springer, Heidelberg (1991)

    Google Scholar 

  13. Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)

    Article  MATH  Google Scholar 

  14. Hofmann, M., Sannella, D.: On behavioural abstraction and behavioural satisfaction in higher-order logic. Theoretical Computer Science 167, 3–45 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  15. Honsell, F., Longley, J., Sannella, D., Tarlecki, A.: Constructive data refinement in typed lambda calculus. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 161–176. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Honsell, F., Sannella, D.: Prelogical relations. CSL 1999 178, 23–43 (2002); Short version In: Proc. Computer Science Logic, CSL 1999, Madrid. Springer LNCS 1683, pp. 546-561 (1999)

    Google Scholar 

  17. Katsumata, S.: Behavioural equivalence and indistinguishability in higher-order typed languages. Selected papers from the 16th Intl. Workshop on Algebraic Development Techniques, Frauenchiemsee. Springer LNCS (2003) (to appear)

    Google Scholar 

  18. Leiß, H.: Second-order pre-logical relations and representation independence. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 298–314. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  19. Ma, Q., Reynolds, J.: Types, abstraction and parametric polymorphism, part 2. In: Schmidt, D., Main, M.G., Melton, A.C., Mislove, M.W., Brookes, S.D. (eds.) MFPS 1991. LNCS, vol. 598, pp. 1–40. Springer, Heidelberg (1991)

    Google Scholar 

  20. Mairson, H.: Outline of a proof theory of parametricity. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 313–327. Springer, Heidelberg (1991)

    Google Scholar 

  21. Milner, R.: An algebraic definition of simulation between programs. In: Proc. 2nd Intl. Joint Conf. on Artificial Intelligence, pp. 481–489. British Computer Society (1971)

    Google Scholar 

  22. Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)

    Google Scholar 

  23. Mitchell, J., Plotkin, G.: Abstract types have existential type. ACM Trans. on Programming Languages and Systems 10(3), 470–502 (1988)

    Article  Google Scholar 

  24. Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  25. Plotkin, G., Power, J., Sannella, D., Tennent, R.: Lax logical relations. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 85–102. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  26. Reynolds, J.: Towards a theory of type structures. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408–425. Springer, Heidelberg (1974)

    Google Scholar 

  27. Reynolds, J.: The Craft of Programming. Prentice Hall, Englewood Cliffs (1981)

    MATH  Google Scholar 

  28. Reynolds, J.: Types, abstraction and parametric polymorphism. In: Proc. 9th IFIP World Computer Congress, Paris, pp. 513–523. North Holland, Amsterdam (1983)

    Google Scholar 

  29. Robinson, E., Rosolini, G.: Reflexive graphs and parametric polymorphism. In: Proc. Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, pp. 364–371. IEEE Computer Society Press, Los Alamitos (1994)

    Chapter  Google Scholar 

  30. Sannella, D., Tarlecki, A.: Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9, 229–269 (1997)

    Article  MATH  Google Scholar 

  31. Schoett, O.: Behavioural correctness of data representations. Science of Computer Programming 14, 43–57 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  32. Strachey, C.: Fundamental concepts in programming languages. Lecture notes from the Intl. Summer School in Programming Languages, Copenhagen (1967)

    Google Scholar 

  33. Tennent, R.: Correctness of data representations in Algol-like languages. In: A Classical Mind: Essays in Honour of C.A.R. Hoare, Prentice Hall, Englewood Cliffs (1994)

    Google Scholar 

  34. Takeuti, I.: An axiomatic system of parametricity. Fundamenta Informaticae 33(4), 397–432 (1998)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Software Engineering, Simula Research Laboratory,  

    Jo Hannay

  2. Laboratory for Foundations of Computer Science, University of Edinburgh,  

    Shin-ya Katsumata & Donald Sannella

Authors
  1. Jo Hannay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shin-ya Katsumata
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Donald Sannella
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Comenius University, Mlynská dolina, 842 48, Bratislava, Slovakia

    Branislav Rovan

  2. Charles University, Prague, Czech Republic

    Peter Vojtáš

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hannay, J., Katsumata, Sy., Sannella, D. (2003). Semantic and Syntactic Approaches to Simulation Relations. In: Rovan, B., Vojtáš, P. (eds) Mathematical Foundations of Computer Science 2003. MFCS 2003. Lecture Notes in Computer Science, vol 2747. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45138-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45138-9_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40671-6

  • Online ISBN: 978-3-540-45138-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation