ECOOP 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA
Fri 20 Jul 2018 11:25 - 11:50 at Zurich II - Types Chair(s): Philipp Haller

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, which includes a plugin for the Eclipse IDE.

Fri 20 Jul

ecoop-2018-papers
11:00 - 12:40: ECOOP Research Papers - Types at Zurich II
Chair(s): Philipp HallerKTH Royal Institute of Technology
ecoop-2018-papers11:00 - 11:25
Research paper
Benjamin W ChungNortheastern University, Paley LiNortheastern University, Francesco Zappa NardelliInria, Jan VitekNortheastern University
DOI
ecoop-2018-papers11:25 - 11:50
Research paper
Joana CamposUniversity of Lisbon, Portugal, Vasco T. VasconcelosUniversity of Lisbon, Portugal
DOI
ecoop-2018-papers11:50 - 12:15
Research paper
Nathalie OostvogelsVrije Universiteit Brussel, Joeri De KosterVrije Universiteit Brussel, Belgium, Wolfgang De MeuterVrije Universiteit Brussel
DOI
ecoop-2018-papers12:15 - 12:40
Research paper
Ugo de'LiguoroUniversità di Torino, Luca PadovaniUniversity of Turin, Italy
DOI