Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 16:45 - 17:07 at Attica - Formalization Chair(s): Eric Koskinen

The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on path-dependent types – types such as x.a.b.T that depend on the runtime value of a path x.a.b to an object. Unfortunately, existing formulations of DOT can model only types of the form x.A which depend on variables rather than general paths. This restriction makes it impossible to model nested module dependencies. Nesting small components inside larger ones is a necessary ingredient of a modular, scalable language. DOT’s variable restriction thus undermines its ability to fully formalize a variety of programming-language features including Scala’s module system, family polymorphism, and covariant specialization.

This paper presents the pDOT calculus, which generalizes DOT to support types that depend on paths of arbitrary length, as well as singleton types to track path equality. We show that naive approaches to add paths to DOT make it inherently unsound, and present necessary conditions for such a calculus to be sound. We discuss the key changes necessary to adapt the techniques of the DOT soundness proofs so that they can be applied to pDOT. Our paper comes with a Coq-mechanized type-safety proof of pDOT. With support for paths of arbitrary length, pDOT can realize DOT’s full potential for formalizing Scala-like calculi.

Wed 23 Oct
Times are displayed in time zone: Beirut change

16:00 - 17:30: FormalizationOOPSLA at Attica
Chair(s): Eric KoskinenStevens Institute of Technology
16:00 - 16:22
Formal Foundations of Serverless ComputingACM SIGPLAN Distinguished Paper Award
Abhinav JangdaUniversity of Massachusetts Amherst, Donald PinckneyUniversity of Massachusetts Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts, Amherst
Link to publication DOI Pre-print
16:22 - 16:45
A Formalization of Java’s Concurrent Access Modes
John BenderUniversity of California, Los Angeles, Jens PalsbergUniversity of California, Los Angeles
16:45 - 17:07
A Path to DOT: Formalizing Fully Path-Dependent Types
Marianna RapoportUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
DOI Pre-print Media Attached
17:07 - 17:30
Qubit Allocation as a Combination of Subgraph Isomorphism and Token Swapping
DOI Pre-print