Guilhem Jaber
ABSTRACT
We introduce a trace semantics for a call-by-value language with full polymorphism and higher-order references. This is an operational game semantics model based on a nominal interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names. The use of polymorphic references leads to violations of parametricity which we counter by closely recoding the disclosure of typing information in the semantics. We prove the model sound for the full language and strengthen our result to full abstraction for a large fragment where polymorphic references obey specific inhabitation conditions.
- S. Abramsky and R. Jagadeesan. A game semantics for generic polymorphism. APAL, 133(1-3), 2005.Google Scholar
- A. Ahmed. Semantics of types for mutable state. PhD thesis, Princeton University, Princeton, NJ, USA, 2004. Google ScholarDigital Library
- A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009. Google ScholarDigital Library
- A. Appel, P.-A. Melliès, C. Richards, and J. Vouillon. A very modal model of a modern, major, general type system. In POPL, 2007. Google ScholarDigital Library
- L. Birkedal, K. Støvring, and J. Thamsborg. Realisability semantics of parametric polymorphism, general references and recursive types. MSCS, 20(04), 2010. Google ScholarDigital Library
- D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. JFP, 22, 2012. Google ScholarDigital Library
- M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal aspects of computing, 13(3-5), 2002.Google Scholar
- D. R. Ghica and N. Tzevelekos. A system-level game semantics. ENTCS, 286, 2012. Google ScholarDigital Library
- D. J. D. Hughes. Hypergame semantics: full completeness for System F. PhD thesis, University of Oxford, 2000.Google Scholar
- J. M. E. Hyland and C.-H. L. Ong. On Full Abstraction for PCF: I, II, and III. Inf. Comput., 163(2), 2000. Google ScholarDigital Library
- G. Jaber. Operational nominal game semantics. In FOSSACS, 2015.Google ScholarCross Ref
- G. Jaber and N. Tabareau. Kripke open bisimulation - a marriage of game semantics and operational techniques. In APLAS, 2015.Google Scholar
- R. Jagadeesan, C. Pitcher and J. Riely. Open bisimulation for aspects. In AOSD, 2007. Google ScholarDigital Library
- A. Jeffrey and J. Rathke. Towards a theory of bisimulation for local names. In LICS, 1999. Google ScholarDigital Library
- A. Jeffrey and J. Rathke. Java Jr: Fully abstract trace semantics for a core java language. In ESOP, 2005. Google ScholarDigital Library
- A. Jeffrey and J. Rathke. Full abstraction for polymorphic pi-calculus. TCS, 390(2-3), 2008. Google ScholarDigital Library
- J. Laird. A fully abstract trace semantics for general references. In ICALP, 2007. Google ScholarDigital Library
- J. Laird. Game semantics for call-by-value polymorphism. In ICALP, 2010. Google ScholarDigital Library
- J. Laird. Game semantics for a polymorphic programming language. J. ACM, 60(4), 2013. Google ScholarDigital Library
- S. Lassen. Eager normal form bisimulation. In LICS, 2005. Google ScholarDigital Library
- S. B. Lassen and P. B. Levy. Typed normal form bisimulation for parametric polymorphism. In LICS, 2008. Google ScholarDigital Library
- G. Longo, K. Milsted, and S. Soloviev. The genericity theorem and parametricity in the polymorphic λ-calculus. TCS, 121(1&2), 1993. Google ScholarDigital Library
- P. Levy and S. Staton. Transition systems over games. In LICS, 2014. Google ScholarDigital Library
- A. S. Murawski, S. J. Ramsay, and N. Tzevelekos. A contextual equivalence checker for IMJ*. In ATVA, 2015.Google ScholarCross Ref
- B. C. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. J. ACM, 47(3), 2000. Google ScholarDigital Library
- J. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, 1983.Google Scholar
- C. Strachey. Fundamental concepts in programming languages. Reprint. Higher-Order and Symbolic Computation, 13(1/2), 2000. Google ScholarDigital Library
- E. Sumii. A complete characterization of observational equivalence in polymorphic λ-calculus with general references. In CSL, 2009. Google ScholarDigital Library
- P. Wadler. Theorems for free! In FPCA, 1989. Google ScholarDigital Library
- A. K. Wright. Simple imperative polymorphism. LASC, 8(4), 1995. Google ScholarDigital Library
- Trace semantics for polymorphic references
Recommendations
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
On polymorphic gradual typing
We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically ...
Realisability semantics of parametric polymorphism, general references and recursive types
We present a realisability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types that include general ...
Comments