Abstract
We propose a “Curry-style” semantics of programs in which a nominal labelled transition system of types, characterizing observable behaviour, is overlaid on a nominal LTS of untyped computation. This leads to a notion of program equivalence as typed bisimulation.
Our semantics reflects the role of types as hiding operators, firstly via an axiomatic characterization of “parallel composition with hiding” which yields a general technique for establishing congruence results for typed bisimulation, and secondly via an example which captures the hiding of implementations in abstract data types: a typed bisimulation for the (Curry-style) lazy \(\lambda \mu \)-calculus with polymorphic types. This is built on an abstract machine for CPS evaluation of \(\lambda \mu \)-terms: we first give a basic typing system for this LTS which characterizes acyclicity of the environment and local control flow, and then refine this to a polymorphic typing system which uses equational constraints on instantiated type variables, inferred from observable interaction, to capture behaviour at polymorphic and abstract types.
Chapter PDF
Similar content being viewed by others
References
S. Abramsky. The lazy \(\lambda \)-calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65–117. Addison Wesley, 1990.
S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163:409–470, 2000.
M. Berger, K. Honda, and N. Yoshida. Sequentiality and the \(\pi \)-calculus. In Proceedings of TLCA 2001, volume 2044 of Lecture Notes in Computer Science. Springer-Verlag, 2001.
M. Berger, K. Honda, and N. Yoshida. Genericity and the \(\pi \)-calculus. Acta Informatica, 42, 2005.
M. Berger, K. Honda, and N. Yoshida. Process types as a descriptive tool for interaction: Control and the \(\pi \)-calculus. In Proceedings of the Rewriting and Typed Lambda-calculi - joint international conference, 2014.
D. R. Ghica and N. Tzevelekos. System level game semantics. Proceedings of MFPS XXVIII, ENTCS volume 286, pages 191 –211. 2012.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.
D. Hughes. Games and definability for System F. In Proceedings of the Twelfth International syposium on Logic in Computer Science, LICS ’97. IEEE Computer Society Press, 1997.
J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Information and Computation, 163:285–408, 2000.
A. Igurashi and N. Kobayashi. A generic type system for the \(\pi \)-calculus. Theoretical Computer Science, 311:121–163, 2004.
Vladimir N. Krupski. The single-conclusion proof logic and inference rules specification. Annals of Pure and Applied Logic, 113:181 – 206, 2002.
J. Laird. A fully abstract trace semantics for general references. In 34th ICALP, volume 4596 of LNCS, pages 667–679. Springer, 2007.
J. Laird. Game semantics of call-by-value polymorphism. In Proceedings of ICALP ’10, number 6198 in LNCS. Springer-Verlag, 2010.
J. Laird. Game semantics for a polymorphic programming language. Journal of the ACM, 60(4), 2013.
S. B. Lassen and P. B. Levy. Typed normal form bisimulation. In Proceedings 16th EACSL Conference on Computer Science and Logic, number 4646 in LNCS, pages 283–297, 2007.
Joachim De Lataillade. Curry-style type isomorphisms and game semantics. MSCS, 18:647–692, 2008.
P. B. Levy and S. Lassen. Typed normal form bisimulation for parametric polymorphism. In Proceedings of LICS 2008, pages 341–552. IEEE press, 2008.
Paul Levy and Sam Staton. Transition systems over games. In CSL-LICS ’14. ACM Press, 2014.
G. Longo. Set-theoretical models of lambda calculus: Theories, expansions and isomorphisms. Annals of Pure and Applied Logic, 24:153–188, 1983.
J. Mitchell and G. Plotkin. Abstract types have existential type. ACM transactions on Programming Languages and Systems, 10(3):470–502, 1988.
M. Parigot. \(\lambda \mu \) calculus: an algorithmic interpretation of classical natural deduction. In Proc. International Conference on Logic Programming and Automated Reasoning, pages 190–201. Springer, 1992.
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015), volume 42, pages 198–211, 2015.
A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013.
J. C. Reynolds. Towards a theory of type structure. In Proceedings of the Programming Symposium, Paris 1974, number 19 in LNCS. Springer, 1974.
D. Sangiorgi. The lazy \(\lambda \)-calculus in a concurrency scenario. Information and Computation, 111:120 –153, 1994.
M. Smyth and G. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761–783, 1982.
N. Tzevelekos and G. Jaber. Trace semantics for polymorphic references. In Proc. LICS’16, pages 585–594. ACM, 2016.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Laird, J. (2020). A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy \(\lambda \mu \)-Calculus. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)