ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Wed 18 Nov 2020 12:40 - 13:00 at SPLASH-V - Scala Symposium

One of the most distinguishing features of the Scala Programming Language is that it features path-dependent types. DOT calculi are a family of formalized programming languages that support path-dependent types. Proving type safety for a programming language with path-dependent types has proven difficult and after a long search Amin et al. presented a type safety proof of the WadlerFest DOT calculus. A more modular and extensible type safety proof for this calculus was later presented by Rapoport et al. This proof has been extended further to show various extensions of the WadlerFest DOT calculus are also sound.

While the proof of Rapoport et al. is simpler and modular than previous proofs, we believe there are more opportunities for simplification. In this talk, we will discuss additional simplifications that are possible for the DOT calculus. The Coq proofs associated with the material of this talk can be found at https://github.com/themaplelab/dot-public.

Wed 18 Nov

Displayed time zone: Central Time (US & Canada) change

09:00 - 14:20
Scala SymposiumScala at SPLASH-V
10:00
5m
Day opening
Welcome to Scala 2020
Scala
Nada Amin Harvard University, Guido Salvaneschi University of St. Gallen, David Richter Technische Universität Darmstadt
10:05
35m
Keynote
Towards a Sound Approximating Compiler for Numerical Kernels (Keynote)
Scala
Eva Darulova MPI-SWS
10:40
20m
Talk
ONNX-Scala: Typeful, Functional Deep Learning / Dotty Meets an Open AI Standard (Open-Source Talk)
Scala
Alexander Merritt Independent
11:00
20m
Paper
Kaizen: A Scalable Concolic Fuzzing Tool for Scala
Scala
Mohammadreza Ashouri University of Potsdam, Germany
11:40
20m
Talk
Asterisk: Secure Programming Language for Smart Contracts (Student Talk)
Scala
Mohammadreza Ashouri University of Potsdam, Germany
12:00
20m
Paper
ScalaPy: Seamless Python Interoperability for Cross-Platform Scala Programs
Scala
Shadaj Laddad University of California at Berkeley, Koushik Sen University of California at Berkeley
12:20
20m
Paper
Semantics-Preserving Inlining for Metaprogramming
Scala
Nicolas Stucki EPFL, Switzerland, Aggelos Biboudis EPFL, Sébastien Doeraene EPFL, Switzerland, Martin Odersky EPFL
12:40
20m
Talk
Toward a Simpler Syntactic Soundness for DOT (Student Talk)
Scala
Ifaz Kabir University of Alberta, Karim Ali University of Alberta
13:00
20m
Day closing
Closing Scala 2020
Scala
Nada Amin Harvard University, Guido Salvaneschi University of St. Gallen, David Richter Technische Universität Darmstadt