If you do not see this message displayed properly, please click here


The Faculty of Informatics is pleased to announce a seminar given by Nada Amin



Types: Safety Net and Springboard
Speaker: Nada Amin
École polytechnique fédérale de Lausanne, Switzerland
Date: Monday, March 27, 2017
Place: USI Lugano Campus, room SI-003, informatics building (Via G. Buffi 13)
Time: 9:30



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.




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.


Host: Prof. Kai Hormann


Faculty of Informatics

Faculty of Informatics
Università della Svizzera italiana
Via Giuseppe Buffi 13
CH-6904 Lugano
Tel.: +41 (0)58 666 46 90
Fax: +41 (0)58 666 45 36
Email: decanato.inf@usi.ch
Web: www.inf.usi.ch
Twitter: @USI_INF


Segui USI@EXPO2015 su Twitter Segui USI@EXPO2015 su Facebook Segui USI@EXPO2015 su Linkedin Segui USI@EXPO2015 su YouTube