A Curry-style Semantics of Interaction: From Untyped to Second-Order Lazy $$\lambda \mu $$-Calculus
| Autor: | James Laird |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Bisimulation
Programming language Computer science Computation Lambda-mu calculus Observable 0102 computer and information sciences 02 engineering and technology Curry computer.software_genre 01 natural sciences 010201 computation theory & mathematics Transition system 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Equivalence (formal languages) computer computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030452308 FoSSaCS |
| DOI: | 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$$\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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|