A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy λμ-Calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 λμ-calculus with polymorphic types. This is built on an abstract machine for CPS evaluation of λμ-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.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures- 23rd International Conference, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
EditorsJean Goubault-Larrecq, Barbara König
Place of PublicationCham, Switzerland
PublisherSpringer
Pages422-441
Number of pages20
ISBN (Print)9783030452308
DOIs
Publication statusPublished - 2020
Event23rd International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12077 LNCS

Conference

Conference23rd International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
CountryIreland
CityDublin
Period25/04/2030/04/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Laird, J. (2020). A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy λμ-Calculus. In J. Goubault-Larrecq, & B. König (Eds.), Foundations of Software Science and Computation Structures- 23rd International Conference, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings (pp. 422-441). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12077 LNCS). Springer. https://doi.org/10.1007/978-3-030-45231-5_22