Trace semantics for polymorphic references

DOI10.1145/2933575.2934509MaRDI QIDQ4635919zbMATH OpenOpenAlexFDO

Authors Guilhem Jaber, Nikos Tzevelekos

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1602.08406, http://qmro.qmul.ac.uk/xmlui/handle/123456789/13081

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

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.

Recommendations

• A Fully Abstract Trace Semantics for General References
• A trace semantics for System F parametric polymorphism
• Type inference for polymorphic references
• A simplified account of polymorphic references
• Realisability semantics of parametric polymorphism, general references and recursive types
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Intensional polymorphism in type-erasure semantics
• Intensional polymorphism in type-erasure semantics
• Intensional polymorphism in type-erasure semantics
• Pragmatic gradual polymorphism with references

Cited in

(13)

• A trace semantics for System F parametric polymorphism
• A curry-style semantics of interaction: from untyped to second-order lazy -calculus
• Complete trace models of state and control
• Operational nominal game semantics
• Realisability semantics of parametric polymorphism, general references and recursive types
• Game semantics for call-by-value polymorphism
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Game semantics for type soundness
• scientific article; zbMATH DE number 7559490 (Why is no real title available?)
• No value restriction is needed for algebraic effects and handlers
• A Fully Abstract Trace Semantics for General References
• Pragmatic gradual polymorphism with references
• First-order store and visibility in name-passing calculi

This page was built for publication: Trace semantics for polymorphic references

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635919)