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

James Laird

doi:10.1007/978-3-030-45231-5_22

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

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

90 Downloads (Pure)

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 language	English
Title of host publication	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
Editors	Jean Goubault-Larrecq, Barbara König
Place of Publication	Cham, Switzerland
Publisher	Springer
Pages	422-441
Number of pages	20
ISBN (Electronic)	9783030452315
ISBN (Print)	9783030452308
DOIs	https://doi.org/10.1007/978-3-030-45231-5_22
Publication status	Published - 2020
Event	23rd 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 2020 → 30 Apr 2020

Publication series

Name	Lecture Notes in Computer Science
Volume	12077
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd 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
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-45231-5_22Licence: CC BY

fos20Licence: CC BY-ND

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 ; Vol. 12077). Springer. https://doi.org/10.1007/978-3-030-45231-5_22

A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy λμ-Calculus. / Laird, James.
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. ed. / Jean Goubault-Larrecq; Barbara König. Cham, Switzerland: Springer, 2020. p. 422-441 (Lecture Notes in Computer Science ; Vol. 12077).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

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. Lecture Notes in Computer Science , vol. 12077, Springer, Cham, Switzerland, pp. 422-441, 23rd 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, 25/04/20. https://doi.org/10.1007/978-3-030-45231-5_22

Laird J. A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy λμ-Calculus. In Goubault-Larrecq J, König B, editors, 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. Cham, Switzerland: Springer. 2020. p. 422-441. (Lecture Notes in Computer Science ). Epub 2020 Apr 17. doi: 10.1007/978-3-030-45231-5_22

Laird, James. / A Curry-style Semantics of Interaction : From Untyped to Second-Order Lazy λμ-Calculus. 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. editor / Jean Goubault-Larrecq ; Barbara König. Cham, Switzerland : Springer, 2020. pp. 422-441 (Lecture Notes in Computer Science ).

@inproceedings{02eb227265d848779fccf0bd43416755,

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

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.",

author = "James Laird",

year = "2020",

doi = "10.1007/978-3-030-45231-5_22",

language = "English",

isbn = "9783030452308",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "422--441",

editor = "Jean Goubault-Larrecq and Barbara K{\"o}nig",

booktitle = "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",

note = "23rd 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 ; Conference date: 25-04-2020 Through 30-04-2020",

}

TY - GEN

T1 - A Curry-style Semantics of Interaction

T2 - 23rd 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

AU - Laird, James

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85084111641&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-45231-5_22

DO - 10.1007/978-3-030-45231-5_22

M3 - Chapter in a published conference proceeding

AN - SCOPUS:85084111641

SN - 9783030452308

T3 - Lecture Notes in Computer Science

SP - 422

EP - 441

BT - 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

A2 - Goubault-Larrecq, Jean

A2 - König, Barbara

PB - Springer

CY - Cham, Switzerland

Y2 - 25 April 2020 through 30 April 2020

ER -

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

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Semantic Types for Verified Program Behaviour

Semantic Structures for Higher-Order Information Flow

James Laird

Cite this

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

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Semantic Types for Verified Program Behaviour

Semantic Structures for Higher-Order Information Flow

Profiles

James Laird

Cite this