Hedy: A Gradual programming language
Felienne Hermans
Learning to program is hard! There are so many things to think of: syntax, data structures, problem solving.
What if we could make a programming language that grows with you, and becomes stricter and more complex over time? In this talk Felienne outlines Hedy: her gradual language for programming education, and how it was designed. She will also reflect on what she has learned from trying Hedy with groups of children and from analyzing the first 500.000 Hedy programs.
Verification with Refinement Types
Ranjit Jhala
The last few decades have seen tremendous strides in various technologies for reasoning about programs. However, we believe these technologies will only become ubiquitous if they can be seamlessly integrated within programming so that programmers can use them continuously throughout the software development lifecycle. In this tutorial, we will learn how refinement types offer a path towards integrating verification into existing host languages, by integrating the compositional nature of types with the expressiveness of logics, and the automation of model checking. We will see how refinements allow the programmer to extend specifications using types, to extend the analysis using SMT and abstract interpretation and finally, to extend verification beyond automatically decidable logical fragments, by allowing programmers to interactively write proofs simply as code in the host language.
The tutorial will include hands-on exercises, so be ready with your laptops!
Growing the Hack language
Francesco Zappa Nardelli
Facebook's main website, ads platform, and much of its internal tooling is implemented in Hack, a language that evolved from PHP by removing the worst features and by adding static typing and modern constructs for asynchronous programming. Its type system is an interesting mixture of ideas from Java, C#, Scala, and OCaml, with flow-sensitive typing thrown in to capture typical PHP idioms and a few unique features. These days developers demand ever richer types, and evolution of the codebase goes hand-in-hand with evolution of the type system and programming language. In this lecture I will review some features recently added to Hack, highlighting the unique entanglement between developer needs, language design challenges, and practical implementation constraints.
Efficient AOT JavaScript compilation
Manuel Serrano
Static compilation, a.k.a., ahead-of-time (AOT) compilation, is an alternative approach to JIT compilation that can combine decent speed, lightweight memory footprint, that can accommodate read-only memory constraints imposed by some devices and some operating systems, and that can be beneficial for brief executions. However, the highly dynamic nature of languages such as JavaScript and Python makes them hard to compile statically and techniques developed for more static general purpose languages do not apply well enough. AOT compilation of dynamic languages requires new optimizations and new implementation techniques.
In this lecture, we will start by studying the main JavaScript compilation difficulties. Then, we will present the most common optimizations all fast implementations, including JIT, use. In the second part, we will present the techniques, optimizations, and typing discipline we have developped to enable efficient AOT JavaScript compilation.