Skip to main content
SpringerLink
Log in

Typed Normal Form Bisimulation

  • Conference paper
Computer Science Logic (CSL 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4646))

Included in the following conference series:

Abstract

Normal form bisimulation is a powerful theory of program equivalence, originally developed to characterize Lévy-Longo tree equivalence and Boehm tree equivalence. It has been adapted to a range of untyped, higher-order calculi, but types have presented a difficulty. In this paper, we present an account of normal form bisimulation for types, including recursive types. We develop our theory for a continuation-passing style calculus, Jump-With-Argument (JWA), where normal form bisimilarity takes a very simple form. We give a novel congruence proof, based on insights from game semantics. A notable feature is the seamless treatment of eta-expansion. We demonstrate the normal form bisimulation proof principle by using it to establish a syntactic minimal invariance result and the uniqueness of the fixed point operator at each type.

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

Access this chapter

Log in via an institution
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.

References

  1. Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. Information and Computation 111(1), 120–153 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  2. Jagadeesan, R., Pitcher, C., Riely, J.: Open bisimulation for aspects. In: Intl. Conf. on Aspect-Oriented Software Development, pp. 209–224. ACM Press, New York (2007)

    Google Scholar 

  3. Lassen, S.B.: Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In: MFPS XV. ENTCS, vol. 20, pp. 346–374. Elsevier, Amsterdam (1999)

    Google Scholar 

  4. Lassen, S.B.: Eager normal form bisimulation. In: 20th LICS, pp. 345–354. IEEE Computer Society Press, Los Alamitos (2005)

    Google Scholar 

  5. Lassen, S.B.: Normal form simulation for McCarty’s amb. In: MFPS XXI. ENTCS, vol. 155, pp. 445–465. Elsevier, Amsterdam (2005)

    Google Scholar 

  6. Lassen, S.B.: Head normal form bisimulation for pairs and the λμ-calculus (extended abstract). In: 21st LICS, pp. 297–306. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

  7. Støvring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: 34th POPL, pp. 63–74. ACM Press, New York (2007)

    Google Scholar 

  8. Abramsky, S.: The lazy λ-calculus. In: Turner, D. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Wesley, Reading (1990)

    Google Scholar 

  9. Gordon, A.D.: Functional Programming and Input/Output. CUP (1994)

    Google Scholar 

  10. Levy, P.B.: Call-By-Push-Value. A Functional/Imperative Synthesis. In: Semantic Struct. in Computation, Springer, Heidelberg (2004)

    Google Scholar 

  11. Levy, P.B.: Adjunction models for call-by-push-value with stacks. Theory and Applications of Categories 14(5), 75–110 (2005)

    MATH  MathSciNet  Google Scholar 

  12. Merro, M., Biasi, C.: On the observational theory of the CPS calculus. In: MFPS XXII. ENTCS, vol. 158, pp. 307–330. Elsevier, Amsterdam (2006)

    Google Scholar 

  13. Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF: I, II, and III. Information and Computation 163(2), 285–408 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  14. Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  15. Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: 13th LICS, pp. 334–344. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  16. Laird, J.: Full abstraction for functional languages with control. In: 12th LICS, pp. 58–67. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  17. Ker, A.D., Nickau, H., Ong, C.H.L.: Innocent game models of untyped lambda-calculus. Theoretical Computer Science 272(1-2), 247–292 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  18. Ker, A.D., Nickau, H., Ong, C.H.L.: Adapting innocent game models for the Böhm tree λ-theory. Theoretical Computer Science 308(1-3), 333–366 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  19. Ong, C.H.L., Gianantonio, P.D.: Games characterizing Lévy-Longo trees. Theoretical Computer Science 312(1), 121–142 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  20. Laird, J.: A categorical semantics of higher-order store. In: 9th Conference on Category Theory and Computer Science. ENTCS, vol. 69, Elsevier, Amsterdam (2003)

    Google Scholar 

  21. Curien, P.L., Herbelin, H.: Computing with abstract Böhm trees. In: Fuji International Symposium on Functional and Logic Programming, pp. 20–39 (1998)

    Google Scholar 

  22. Danos, V., Herbelin, H., Regnier, L.: Game semantics and abstract machines. In: 11th LICS, pp. 394–405. IEEE Computer Society Press, Los Alamitos (1996)

    Google Scholar 

  23. Levy, P.B.: Infinite trace equivalence. In: MFPS XXI. ENTCS, vol. 155, pp. 467–496. Elsevier, Amsterdam (2006)

    Google Scholar 

  24. Levy, P.B.: Game semantics using function inventories.Talk given at Geometry of Computation 2006, Marseille (2006)

    Google Scholar 

  25. Laird, J.: A fully abstract trace semantics for general references. In: 34th ICALP. LNCS, vol. 4596, Springer, Heidelberg (2007)

    Google Scholar 

  26. Hyland, J.M.E., Ong, C.H.L.: Pi-calculus, dialogue games and PCF. In: 7th FPCA, pp. 96–107. ACM Press, New York (1995)

    Chapter  Google Scholar 

  27. Fiore, M.P., Honda, K.: Recursive types in games: Axiomatics and process representation. In: 13th LICS, pp. 345–356. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  28. Thielecke, H.: Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh (1997)

    Google Scholar 

  29. Thielecke, H.: Contrasting exceptions and continuations, October 2001 (unpublished)

    Google Scholar 

  30. Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Revised edn., North-Holland, Amsterdam (1984)

    Google Scholar 

  31. Pitts, A.M.: Relational properties of domains. Information and Computation 127, 66–90 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  32. Birkedal, L., Harper, R.: Operational interpretations of recursive types in an operational setting (summary). In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  33. Lassen, S.B.: Relational reasoning about contexts. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics.CUP, pp. 91–135 (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Google, Inc.,  

    Soren B. Lassen

  2. University of Birmingham, U.K.

    Paul Blain Levy

Authors
  1. Soren B. Lassen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul Blain Levy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jacques Duparc Thomas A. Henzinger

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lassen, S.B., Levy, P.B. (2007). Typed Normal Form Bisimulation. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74915-8_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74914-1

  • Online ISBN: 978-3-540-74915-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation