Document Open Access Logo

Towards Strong Normalization for Dependent Object Types (DOT)

Authors Fei Wang, Tiark Rompf

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.27.pdf
  • Filesize: 0.69 MB
  • 25 pages

Document Identifiers

Author Details

Fei Wang
Tiark Rompf

Cite AsGet BibTex

Fei Wang and Tiark Rompf. Towards Strong Normalization for Dependent Object Types (DOT). In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 27:1-27:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.27

Abstract

The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar languages, unifying functional programming, object oriented programming and ML-style module systems. Following the recent type soundness proof for DOT, the present paper aims to establish stronger meta-theoretic properties. The main result is a fully mechanized proof of strong normalization for D_<:, a variant of DOT that excludes recursive functions and recursive types. We further discuss techniques and challenges for adding recursive types while maintaining strong normalization, and demonstrate that certain variants of recursive self types can be integrated successfully.
Keywords
  • Scala
  • DOT
  • strong normalization
  • logical relations
  • recursive types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel. Polarised subtyping for sized types. Mathematical Structures in Computer Science, 18:797-822, 10 2008. Google Scholar
  2. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In PPDP, 2003. Google Scholar
  3. Amal J. Ahmed. Semantics of types for mutable state. PhD thesis, Princeton University, 2004. Google Scholar
  4. Amal J. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006. Google Scholar
  5. Amal J. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006. Google Scholar
  6. Nada Amin. Dependent Object Types. PhD thesis, EPFL, August 2016. Google Scholar
  7. Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The essence of dependent object types. In A List of Successes That Can Change the World, volume 9600 of Lecture Notes in Computer Science, pages 249-272. Springer, 2016. Google Scholar
  8. Nada Amin, Adriaan Moors, and Martin Odersky. Dependent object types. In FOOL, 2012. Google Scholar
  9. Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. In POPL, 2017. Google Scholar
  10. Nada Amin, Tiark Rompf, and Martin Odersky. Foundations of path-dependent types. In OOPSLA, 2014. Google Scholar
  11. Nada Amin and Ross Tate. Java and scala’s type systems are unsound: the existential crisis of null pointers. In OOPSLA, pages 838-848. ACM, 2016. Google Scholar
  12. Andrew W. Appel and David A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-683, 2001. Google Scholar
  13. David Aspinall and Adriana Compagnoni. Subtyping dependent types. Theoretical Computer Science, 266(1):273-309, 2001. Google Scholar
  14. H. P. Barendregt. Handbook of logic in computer science. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, Handbook of Logic in Computer Science, chapter Lambda Calculi with Types. Oxford University Press, 1992. Google Scholar
  15. Nicholas R. Cameron, James Noble, and Tobias Wrigstad. Tribal ownership. In OOPSLA, 2010. Google Scholar
  16. Peter S. Canning, William R. Cook, Walter L. Hill, Walter G. Olthoff, and John C. Mitchell. F-bounded polymorphism for object-oriented programming. In FPCA, pages 273-280. ACM, 1989. Google Scholar
  17. Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining proofs and programs in a dependently typed language. In POPL, pages 33-46. ACM, 2014. Google Scholar
  18. Dave Clarke, Sophia Drossopoulou, James Noble, and Tobias Wrigstad. Tribe: a simple virtual class calculus. In AOSD, 2007. Google Scholar
  19. Vincent Cremet, François Garillot, Sergueï Lenglet, and Martin Odersky. A core calculus for Scala type checking. In MFCS, 2006. Google Scholar
  20. Olivier Danvy and Jacob Johannsen. Inter-deriving semantic artifacts for object-oriented programming. J. Comput. Syst. Sci., 76(5):302-323, 2010. Google Scholar
  21. Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. On inter-deriving small-step and big-step semantics: A case study for storeless call-by-need evaluation. Theor. Comput. Sci., 435:21-42, 2012. Google Scholar
  22. Derek Dreyer and Andreas Rossberg. Mixin' up the ML module system. In ICFP, 2008. Google Scholar
  23. Erik Ernst. Family polymorphism. In ECOOP, 2001. Google Scholar
  24. Erik Ernst. Higher-order hierarchies. In ECOOP, 2003. Google Scholar
  25. Erik Ernst, Klaus Ostermann, and William R. Cook. A virtual class calculus. In POPL, 2006. Google Scholar
  26. Peng Fu and Aaron Stump. Self types for dependently typed lambda encodings. In RTA-TLCA, volume 8560 of Lecture Notes in Computer Science, pages 224-239. Springer, 2014. Google Scholar
  27. Vaidas Gasiunas, Mira Mezini, and Klaus Ostermann. Dependent classes. In OOPSLA, 2007. Google Scholar
  28. Giorgio Ghelli. Termination of system f-bounded: A complete proof. Inf. Comput., 139(1):39-56, 1997. Google Scholar
  29. Silvia Ghilezan. Strong normalization and typability with intersection types. Notre Dame Journal of Formal Logic, 37(1):44-52, 1996. Google Scholar
  30. Eduardo Giménez. Structural recursive definitions in type theory. In ICALP, volume 1443 of Lecture Notes in Computer Science, pages 397-408. Springer, 1998. Google Scholar
  31. Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  32. C. A. Gunter and D. Rémy. A proof-theoretic assesment of runtime type errors. Technical Report 11261-921230-43TM, AT&T Bell Laboratories, 1993. Google Scholar
  33. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL, 1994. Google Scholar
  34. DeLesley S. Hutchins. Pure subtype systems. In POPL, 2010. Google Scholar
  35. Gilles Kahn. Natural semantics. In STACS, 1987. Google Scholar
  36. Xavier Leroy. Manifest types, modules and separate compilation. In POPL, 1994. Google Scholar
  37. David Macqueen. Using dependent types to express modular structure. In POPL, 1986. Google Scholar
  38. Dmitry Petrashko Martin Odersky, Guillaume Martres. Implementing higher-kinded types in dotty. In Scala, 2016. Google Scholar
  39. David A. McAllester, J. Kucan, and D. F. Otth. A proof of strong normalization of F₂, F_ω and beyond. Inf. Comput., 121(2):193-200, 1995. Google Scholar
  40. Adriaan Moors, Frank Piessens, and Martin Odersky. Safe type-level abstraction in Scala. In FOOL, 2008. Google Scholar
  41. Nathaniel Nystrom, Stephen Chong, and Andrew C. Myers. Scalable extensibility via nested inheritance. In OOPSLA, 2004. Google Scholar
  42. Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. A nominal theory of objects with dependent types. In ECOOP, 2003. Google Scholar
  43. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. Functional big-step semantics. In ESOP, 2016. Google Scholar
  44. Benjamin C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, December 1991. Google Scholar
  45. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program., 60-61:17-139, 2004. Google Scholar
  46. John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363-397, 1998. Google Scholar
  47. Tiark Rompf and Nada Amin. Type soundness for dependent object types (DOT). In OOPSLA, pages 624-641. ACM, 2016. Google Scholar
  48. Andreas Rossberg. 1ML - core and modules united (F-ing first-class modules). In ICFP, 2015. Google Scholar
  49. Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. F-ing modules. J. Funct. Program., 24(5):529-607, 2014. Google Scholar
  50. Jeremy Siek. Type safety in three easy lemmas. http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html, 2013.
  51. Martin Steffen. Polarized higher-order subtyping. PhD thesis, University of Erlangen-Nuremberg, 1997. Google Scholar
  52. Aaron Stump. The calculus of dependent lambda eliminations. Technical report, The University of Iowa (under submission to JFP), 2016. URL: http://homepage.cs.uiowa.edu/~astump/papers/cedille-draft.pdf.
  53. Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich. Termination casts: A flexible approach to termination with general recursion. In PAR, volume 43 of EPTCS, pages 76-93, 2010. Google Scholar
  54. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact