License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2018.13
URN: urn:nbn:de:0030-drops-92182
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9218/
Go to the corresponding LIPIcs Volume Portal

Campos, Joana ; Vasconcelos, Vasco T.

Dependent Types for Class-based Mutable Objects

pdf-format:
LIPIcs-ECOOP-2018-13.pdf (0.5 MB)

Abstract

We present an imperative object-oriented language featuring a dependent type system designed to support class-based programming and inheritance. Programmers implement classes in the usual imperative style, and may take advantage of a richer dependent type system to express class invariants and restrictions on how objects are allowed to change and be used as arguments to methods. By way of example, we implement insertion and deletion for binary search trees in an imperative style, and come up with types that ensure the binary search tree invariant. This is the first dependently-typed language with mutable objects that we know of to bring classes and index refinements into play, enabling types (classes) to be refined by indices drawn from some constraint domain. We give a declarative type system that supports objects whose types may change, despite being sound. We also give an algorithmic type system that provides a precise account of quantifier instantiation in a bidirectional style, and from which it is straightforward to read off an implementation. Moreover, all the examples in the paper have been run, compiled and executed in a fully functional prototype that includes a plugin for the Eclipse IDE.

BibTeX - Entry

@InProceedings{campos_et_al:LIPIcs:2018:9218,
  author =	{Joana Campos and Vasco T. Vasconcelos},
  title =	{{Dependent Types for Class-based Mutable Objects}},
  booktitle =	{32nd European Conference on Object-Oriented Programming  (ECOOP 2018)},
  pages =	{13:1--13:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Todd Millstein},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9218},
  URN =		{urn:nbn:de:0030-drops-92182},
  doi =		{10.4230/LIPIcs.ECOOP.2018.13},
  annote =	{Keywords: dependent types, index refinements, mutable objects, type systems}
}

Keywords: dependent types, index refinements, mutable objects, type systems
Collection: 32nd European Conference on Object-Oriented Programming (ECOOP 2018)
Issue Date: 2018
Date of publication: 10.07.2018
Supplementary Material: ECOOP Artifact Evaluation approved artifact available at http://dx.doi.org/10.4230/DARTS.4.3.1

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI