This is not a Type: Gradual typing in practice
Event details
| Date | 08.04.2016 |
| Hour | 15:00 › 16:00 |
| Location | |
| Category | Conferences - Seminars |
by Prof. Jan Vitek
Abstract
"Do well-typed programs go wrong?" "Of course they do, dear, even the finest programs written using the best of type systems.” “But then, why bother?” “Because it is the way of the world child.” The vast majority of programs written today are written in languages with a single, unconstrained, type; in other words they ignore four decade of research in programming languages. But all is not lost. An idea --referred to, for the lack of better name, as gradual typing-- has gained hold in both academe and industry. At heart, gradual typing is about incrementally decorating untyped programs with type annotations and obtaining (partial) correctness. Not surprisingly soundness has a very different meaning in academic efforts and industrial ones. This talk will attempt to explain what it means for a variable x to have type T and argue that soundness must be revisited in this new age. Examples from our experience implementing and evaluating gradual type systems for languages such as JavaScript, Thorn and Racket will illustrate the talk. Some hopeful conclusions will be drawn.
Bio
Prof. Vitek has a foot in the new world where he is part of the PRL lab at Northeastern University and the old one where he is the principal investigator on an ERC Advanced grant on language evolution. He does research in programming languages during the day but dreams of data science at night. He is actively recruiting students and postdocs.
More information
Abstract
"Do well-typed programs go wrong?" "Of course they do, dear, even the finest programs written using the best of type systems.” “But then, why bother?” “Because it is the way of the world child.” The vast majority of programs written today are written in languages with a single, unconstrained, type; in other words they ignore four decade of research in programming languages. But all is not lost. An idea --referred to, for the lack of better name, as gradual typing-- has gained hold in both academe and industry. At heart, gradual typing is about incrementally decorating untyped programs with type annotations and obtaining (partial) correctness. Not surprisingly soundness has a very different meaning in academic efforts and industrial ones. This talk will attempt to explain what it means for a variable x to have type T and argue that soundness must be revisited in this new age. Examples from our experience implementing and evaluating gradual type systems for languages such as JavaScript, Thorn and Racket will illustrate the talk. Some hopeful conclusions will be drawn.
Bio
Prof. Vitek has a foot in the new world where he is part of the PRL lab at Northeastern University and the old one where he is the principal investigator on an ERC Advanced grant on language evolution. He does research in programming languages during the day but dreams of data science at night. He is actively recruiting students and postdocs.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host: Viktor Kuncak