@article{tanabe2024pldi,
  author = {Atsushi Igarashi and Shota Ozaki and Taro Sekiyama and Yudai Tanabe},
  title = {Space-Efficient Polymorphic Gradual Typing, Mostly Parametric},
  journal = {Proceedings of the ACM on Programming Languages, Volume 8, Issue PLDI},
  year = 2024,
  month = jun,
  date = {2024-06-24},
  doi = {10.1145/3656441},
  url = {https://dl.acm.org/doi/10.1145/3656441},
  abstract = {Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficiency problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop {$\lambda$C${}^{\forall}_{mp}$}, which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present {$\lambda$S${}^{\forall}_{mp}$}, a space-efficient version of {$\lambda$C${}^{\forall}_{mp}$}, and prove that {$\lambda$S${}^{\forall}_{mp}$} programs can be executed in a space-efficient manner and that translation from {$\lambda$C${}^{\forall}_{mp}$} to {$\lambda$S${}^{\forall}_{mp}$} is type- and semantics-preserving.}
}