| Zdroj: |
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 |
| Popis: |
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. |
