Document Open Access Logo

On Satisfiability of Nominal Subtyping with Variance

Authors Aleksandr Misonizhnik, Dmitry Mordvinov

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.7.pdf
  • Filesize: 0.56 MB
  • 20 pages

Document Identifiers

Author Details

Aleksandr Misonizhnik
  • JetBrains Research, Saint Petersburg State University, Russia
Dmitry Mordvinov
  • JetBrains Research, Saint Petersburg State University, Russia

Acknowledgements

We thank Sophia Drossopoulou, Dmitry Boulytchev and anonymous reviewers for their insight and comments that significantly improved the manuscript.

Cite As Get BibTex

Aleksandr Misonizhnik and Dmitry Mordvinov. On Satisfiability of Nominal Subtyping with Variance. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ECOOP.2019.7

Abstract

Nominal type systems with variance, the core of the subtyping relation in object-oriented programming languages like Java, C# and Scala, have been extensively studied by Kennedy and Pierce: they have shown the undecidability of the subtyping between ground types and proposed the decidable fragments of such type systems. However, modular verification of object-oriented code may require reasoning about the relations of open types. In this paper, we formalize and investigate the satisfiability problem for nominal subtyping with variance. We define the problem in the context of first-order logic. We show that although the non-expansive ground nominal subtyping with variance is decidable, its satisfiability problem is undecidable. Our proof uses a remarkably small fragment of the type system. In fact, we demonstrate that even for the non-expansive class tables with only nullary and unary covariant and invariant type constructors, the satisfiability of quantifier-free conjunctions of positive subtyping atoms is undecidable. We discuss this result in detail, as well as show one decidable fragment and a scheme for obtaining other decidable fragments.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
  • Software and its engineering → Object oriented languages
  • Software and its engineering → Automated static analysis
  • Software and its engineering → Polymorphism
  • Software and its engineering → Inheritance
Keywords
  • nominal type systems
  • structural subtyping
  • first-order logic
  • decidability
  • software verification

Metrics

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

References

  1. Mike Barnett, K Rustan M Leino, and Wolfram Schulte. The Spec#programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 49-69. Springer, 2004. Google Scholar
  2. Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. In Handbook of Model Checking, pages 305-343. Springer, 2018. Google Scholar
  3. Leonardo Mendonça de Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69-77, 2011. Google Scholar
  4. ECMA ECMA. 335: Common language infrastructure (CLI), 2005. Google Scholar
  5. Burak Emir, Andrew Kennedy, Claudio V. Russo, and Dachuan Yu. Variance and Generalized Constraints for C# Generics. In ECOOP, volume 4067 of Lecture Notes in Computer Science, pages 279-303. Springer, 2006. Google Scholar
  6. Alexandre Frey. Satisfying Subtype Inequalities in Polynomial Space. In SAS, volume 1302 of Lecture Notes in Computer Science, pages 265-277. Springer, 1997. Google Scholar
  7. Radu Grigore. Java generics are Turing complete. In POPL, pages 73-85. ACM, 2017. Google Scholar
  8. Andrew J Kennedy and Benjamin C Pierce. On decidability of nominal subtyping with variance, 2007. Google Scholar
  9. Viktor Kuncak and Martin C. Rinard. Structural Subtyping of Non-Recursive Types is Decidable. In LICS, pages 96-107. IEEE Computer Society, 2003. Google Scholar
  10. Mark Lillibridge. Translucent sums: A foundation for higher-order module systems. PhD thesis, Carnegie Mellon University, 1997. Google Scholar
  11. Joachim Niehren, Tim Priesnitz, and Zhendong Su. Complexity of Subtype Satisfiability over Posets. In ESOP, volume 3444 of Lecture Notes in Computer Science, pages 357-373. Springer, 2005. Google Scholar
  12. Martin Odersky. Scaling DOT to Scala-soundness, 2016. Google Scholar
  13. Emil L Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52(4):264-268, 1946. Google Scholar
  14. Vaughan R. Pratt and Jerzy Tiuryn. Satisfiability of Inequalities in a Poset. Fundam. Inform., 28(1-2):165-182, 1996. Google Scholar
  15. Andreas Rossberg. Undecidability of OCaml type checking, 1999. Google Scholar
  16. Elena Sherman, Brady J. Garvin, and Matthew B. Dwyer. Deciding Type-Based Partial-Order Constraints for Path-Sensitive Analysis. ACM Trans. Softw. Eng. Methodol., 24(3):15:1-15:33, 2015. Google Scholar
  17. Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen. The first-order theory of subtyping constraints. In POPL, pages 203-216. ACM, 2002. Google Scholar
  18. Todd L. Veldhuizen. C++ Templates are Turing complete, 2003. Google Scholar
  19. Mirko Viroli. On the recursive generation of parametric types. Technical report, Technical Report DEIS-LIA-00-002, Universita di Bologna, 2000. 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 About DROPS Imprint Privacy Contact