Gradual typing has become a standard mechanism for both progressively adding types to dynamically typed languages and liberalising existing type systems, and recent developments have produced the Gradualizer and Abstracting Gradual Typing (AGT) for systematically lifting a typed language to a corresponding gradual language. AGT applies the principles of abstract interpretation to a language’s underlying predicates and functions: we have used this technique to build a library in the dependently typed language Agda for automatically generating different type systems over the same language of terms. Our mechanisation takes an abstract description of a type system indexed by a functor and then generates a variety of different type systems, including gradual typing.
| Automating Gradual Typing Slides (stop16-automating-gradual-typing-slides.pdf) | 75KiB |
Programming languages PhD student at VUW working on Grace.
Sun 17 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:05 - 12:25 | |||
10:05 50mTalk | Optional Typing in Dart: Purity and Practice STOP Gilad Bracha Google Pre-print | ||
10:55 30m | Beyond Types: Extending the Gradual Guarantee STOP James Noble Victoria University of Wellington, Michael Homer Victoria University of Wellington, Timothy Jones Victoria University of Wellington, Sophia Drossopoulou Imperial College London, Andrew Black Portland State University, Kim Bruce Pomona College Link to publication | ||
11:25 30m | Gradual Typing for Delimited Continuations STOP Link to publication | ||
11:55 30mTalk | Automating Gradual Typing STOP Timothy Jones Victoria University of Wellington Link to publication File Attached | ||
