Types: Safety Net and Springboard

Abstract:

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, the Scala programming language unifies concepts from object and module systems.
In particular, objects can contain type members, which can be selected as types, called path-dependent types. Focusing on path-dependent types, we develop a type-theoretic foundation for Scala: the calculus of Dependent Object Types (DOT). The DOT calculus finally grounds languages like Scala in firm theory. The DOT calculus helps in finding bugs in Scala, and in understanding feature interaction better as well as requirements. The DOT calculus serves as a good basis for future work which studies extensions or encodings on top of the core, bridging the gap from DOT to Scala, i.e. from an idealized formal model to a full programming language that's widely used in industry.

In the second part, we apply Scala's type system reaping benefits beyond type safety. Using the Lightweight Modular Staging (LMS) framework, we review a principled approach, driven by types, to generative programming: writing expressive high-level programs that generate fast low-level code at runtime. We show how to extend the approach to verification by generating annotations that enable the low-level code to be independently validated for safety or functional correctness. We illustrate the LMS motto "abstraction without regret" with a small and fast SQL query engine, and a high-level, fast and safe HTTP parser.

Biography:

Nada Amin is a member of the Scala team at EPFL, where she studies type systems and hacks on programming languages. For her PhD thesis, she developed a sound design for Dependent Object Types (DOT), a type-theoretic foundation for programming languages like Scala. She has also published papers on techniques for proving type soundness, and on generative programming and verification. As a software engineer, she has contributed to Clojure's core.logic and Google's Closure compiler. She's loved helping others learn to program ever since tutoring SICP as an undergraduate lab assistant at MIT.