ISSTA/ECOOP 2024
Mon 16 - Fri 20 September 2024 Vienna, Austria

This program is tentative and subject to change.

Fri 20 Sep 2024 15:30 - 16:00 at EI 2 Pichelmayer - FTfJP Session 3

Intersection and union types are advance programming features and are able to encode various classical programming constructs. Significance of intersection and union types is visible by the fact that these types are available in many modern programming languages including Scala, TypeScript and Ceylon. (Un-tagged) Union types are normally eliminated using a type-based switch construct. The branches of the switch construct may overlap thus resulting in an ambiguous semantics. Recently, a disjointness based approach so called \u has been proposed to deal with ambiguity in (un-tagged) union elimination. When studied with intersection types and parametric polymorphism, \u poses an un-intuitive ground type restriction on type variable bounds. This restriction reduces the expressiveness of the calculus. In this paper, we propose a novel disjointness algorithm based on union splittable types. The novel disjointness algorithm does not require ground type restriction on type variable bounds. Therefore, the resulting calculus is more expressive. We also prove soundness and completeness of our disjointness algorithm (without parametric polymorphism) w.r.t disjointness specifications for monomorphic \u. All the metatheory of this paper has been formalized in Coq theorem prover.

This program is tentative and subject to change.

Fri 20 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:30 - 17:30
FTfJP Session 3FTfJP at EI 2 Pichelmayer
15:30
30m
Talk
Disjoint Polymorphism with Intersection and Union Types
FTfJP
Baber Rehman University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
16:00
30m
Talk
Coeffects for MiniJava: Cf-Mj
FTfJP
Paola Giannini University of Eastern Piedmont, Giulio Duso University of Eastern Piedmont
16:30
30m
Talk
Dafny vs. Dala: Experience with Mechanising Language Design
FTfJP
James Noble Independent. Wellington, NZ, Julian Mackay Victoria University of Wellington, Tobias Wrigstad Uppsala University, Andrew Fawcett Victoria University of Wellington, Michael Homer Victoria University of Wellington
17:00
30m
Talk
Incrementalizing Polynomial Functors
FTfJP
Timon Böhler Technical University of Darmstadt, David Richter Technical University of Darmstadt, Mira Mezini TU Darmstadt