Wed 17 Jul 2019 14:30 - 14:50 at Track 1 - Types

We describe the algorithm implemented in the Julia programming language runtime to decide subtyping on a simple type system with union types, covariant tuples, and literals. This algorithm is immune from the space-explosion and expressiveness problems of standard algorithms that normalise types into disjunctive normal form ahead-of-time. We prove this algorithm correct and complete against a semantic-subtyping denotational model in Coq.

Wed 17 Jul

ecoop-2019-papers
13:30 - 15:10: ECOOP Research Papers - Types at Track 1
ecoop-2019-papers13:30 - 13:50
Research paper
Richard RobertsVictoria University of Wellington, Stefan MarrUniversity of Kent, Michael HomerVictoria University of Wellington, James NobleVictoria University of Wellington
ecoop-2019-papers13:50 - 14:10
Research paper
Jan de Muijnck-HughesUniversity of Glasgow, Wim VanderbauwhedeUniversity of Glasgow
ecoop-2019-papers14:10 - 14:30
Research paper
Alen ArslanagićUniversity of Groningen, Jorge A. PérezUniversity of Groningen, The Netherlands, Erik VoogdUniversity of Groningen
Pre-print
ecoop-2019-papers14:30 - 14:50
Research paper
Benjamin ChungNortheastern University, Francesco Zappa NardelliInria, Jan VitekNortheastern University
ecoop-2019-papers14:50 - 15:10
Research paper
Aleksandr MisonizhnikSaint-Petersburg State University, Dmitry MordvinovSaint-Petersburg State University, JetBrains Research