ECOOP 2022
Mon 6 June - Thu 7 July 2022 Berlin, Germany
Thu 9 Jun 2022 14:30 - 14:50 at Aurora Borealis 1 - Language Implementation Chair(s): Guido Salvaneschi
Thu 23 Jun 2022 18:30 - 19:00 at Zoom - VCOOP 6 Chair(s): Elisa Gonzalez Boix

Union types are nowadays a common feature in many modern programming languages. This paper investigates a formulation of union types with an elimination construct that enables case analysis (or switches) on types. The interesting aspect of this construct is that each clause must operate on disjoint types. By using disjoint switches, it is possible to ensure exhaustiveness (i.e. all possible cases are handled), and that none of the cases overlap. In turn, this means that the order of the cases does not matter and that reordering the cases has no impact on the semantics, helping with program understanding and refactoring. While implemented in the Ceylon language, disjoint switches have not been formally studied in the research literature, although a related notion of disjointness has been studied in the context of disjoint intersection types. We study union types with disjoint switches formally and in a language independent way. We first present a simplified calculus, called the union calculus (λu), which includes disjoint switches and prove several results, including type soundness and determinism. The notion of disjointness in λu is in essence the dual notion of disjointness for intersection types. We then present a more feature-rich formulation of λu , which includes intersection types, distributive subtyping and a simple form of nominal types. This extension reveals new challenges. Those challenges require us to depart from the dual notion of disjointness for intersection types, and use a more general formulation of disjointness instead. Among other applications, we show that disjoint switches provide an alternative to certain forms of overloading, and that they enable a simple approach to nullable (or optional) types. All the results about λu and its extensions have been formalized in the Coq theorem prover.

Thu 9 Jun

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

13:30 - 15:00
Language ImplementationHub Talks / Research Papers at Aurora Borealis 1
Chair(s): Guido Salvaneschi University of St. Gallen
13:30
20m
Talk
Benchmarking, analysis, and optimization of serverless function snapshotsHub Talk
Hub Talks
Dmitrii Ustiugov ETH Zurich, Switzerland, Plamen Petrov , Marios Kogias Microsoft Research, Edouard Bugnion EPFL, Boris Grot University of Edinburgh, UK
Link to publication DOI
13:50
20m
Talk
Synchron - An API and Runtime for Embedded SystemsECOOP 2022
Research Papers
Abhiroop Sarkar Chalmers University of Technology, Bo Joel Svensson Chalmers University of Technology, Sweden, Mary Sheeran Chalmers
Pre-print
14:10
20m
Talk
Functional Programming with DatalogECOOP 2022
Research Papers
André Pacak JGU Mainz, Sebastian Erdweg JGU Mainz
14:30
20m
Talk
Union Types with Disjoint SwitchesArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Baber Rehman The University of Hong Kong, Xuejing Huang The University of Hong Kong, Ningning Xie University of Toronto, Bruno C. d. S. Oliveira University of Hong Kong

Thu 23 Jun

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

18:30 - 19:00
VCOOP 6Research Papers at Zoom
Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel, Belgium
18:30
30m
Talk
Union Types with Disjoint SwitchesArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Baber Rehman The University of Hong Kong, Xuejing Huang The University of Hong Kong, Ningning Xie University of Toronto, Bruno C. d. S. Oliveira University of Hong Kong