Types: Safety Net and Springboard
Staff - Faculty of Informatics
Start date: 27 March 2017
End date: 28 March 2017
|
|||||||||||
|
|||||||||||
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 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. |
|||||||||||
|
|||||||||||
|