Abstracting Gradual Typing
Event details
| Date | 28.06.2016 |
| Hour | 12:00 › 13:00 |
| Speaker | Éric Tanter, University of Chile |
| Location | |
| Category | Conferences - Seminars |
(joint work with Ronald Garcia and Alison Clark, presented at POPL’16)
Abstract:
Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs.
We propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning.
Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the subject-reduction proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not recourse to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof-reduction.
Gradual languages designed with the AGT approach satisfy, by construction, the refined criteria for gradual typing set forth by Siek and colleagues.
Time permitting, we will report on recent developments in applying AGT to different typing disciplines, such as effects and security typing.
Bio:
Éric Tanter is a Full Professor in the Computer Science Department of the University of Chile, where he founded the PLEIAD laboratory. He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming.
Abstract:
Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs.
We propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning.
Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the subject-reduction proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not recourse to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof-reduction.
Gradual languages designed with the AGT approach satisfy, by construction, the refined criteria for gradual typing set forth by Siek and colleagues.
Time permitting, we will report on recent developments in applying AGT to different typing disciplines, such as effects and security typing.
Bio:
Éric Tanter is a Full Professor in the Computer Science Department of the University of Chile, where he founded the PLEIAD laboratory. He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming.
Links
Practical information
- Informed public
- Free
Contact
- Host: Martin Odersky