Type inference for polymorphic references

DOI10.1016/0890-5401(90)90018-DzbMath0705.68028OpenAlexW2151156765WikidataQ55222540 ScholiaQ55222540MaRDI QIDQ918190

Mads Tofte

Publication date: 1990

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(90)90018-d

zbMATH Keywords

operational semanticsstandard MLsoundnessfunctional programming languagespolymorphic type inference

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items

Simple type inference for term graph rewriting systems ⋮ A simplified account of polymorphic references ⋮ Types for modules ⋮ Sharing analysis based on type inference ⋮ A note on ``A simplified account of polymorphic references ⋮ A record calculus with principal types ⋮ An imperative object calculus ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ A linear logical framework ⋮ No value restriction is needed for algebraic effects and handlers ⋮ Weak polymorphism can be sound ⋮ Operational interpretations of an extension of F_ω with control operators ⋮ Unnamed Item ⋮ Co-induction in relational semantics ⋮ A type soundness proof for variables in LCF ML ⋮ <scp>OutsideIn(X)</scp>Modular type inference with local assumptions ⋮ Weak updates and separation logic ⋮ A Classical Realizability Model for a Semantical Value Restriction ⋮ Mechanized metatheory revisited ⋮ A cost-effective estimation of uncaught exceptions in Standard ML programs

Uses Software

• ML

Cites Work

• Co-induction in relational semantics
• A theory of type polymorphism in programming
• Edinburgh LCF. A mechanized logic of computation
• The Principal Type-Scheme of an Object in Combinatory Logic
• Unnamed Item
• Unnamed Item