Gradual Programming with Hedy and Creating Programming Languages in non-English
Felienne Hermans
Verona: co-designing the type system, concurrency model, and runtime system
Sophia Drossopoulou
Verona is a language designed and implemented by teams at Microsoft, Uppsalla and Imperial College. Building on the teams’ experiences with Pony, the new language aims to support high-level, high-performance, highly-convenience, safe systems programming. Verona extends the actor paradigm with asynchronous execution so that multiple actors may form temporal alliances and execute behaviours in concert. It has an ownership-based type system that ensures data race freedom and supports fine-grained, region-specific garbage collection. I will introduce Verona through examples and explore the design space of causal ordering for behaviours and their ramifications when reasoning about Verona. I will outline the implementation of a C++ runtime and compare Verona to Pony.
Interpreters: Everywhere and All the Time
Stefan Marr
Implementers often start with an interpreter to sketch how a language may work. They are easy to implement and great to experiment with. However, they are also an essential part of dynamic language implementations. We will talk about the basics of abstract syntax trees, bytecodes, and how these ideas can be used to implement a language. We will also look into optimizations for interpreters: how AST and bytecode interpreters can use run-time feedback to improve performance, and discuss how super nodes and super instructions allows us to make effective use of modern CPUs.
A Brief Introduction to Just-in-Time Compilation
Stefan Marr
Since the early days of object-oriented languages, run-time polymorphism has been a challenge for implementers. Smalltalk and Self pushed many ideas to an extreme, their implementers had to invent techniques such as: lookup caches, tracing and method-based compilation, deoptimization, and maps. While these ideas originated in the '80s and ‘90s, they are key ingredients of today’s just-in-time compilers for Java, Ruby, Python, JavaScript.
JavaScript AOT compilation
Manuel Serrano
JavaScript is particularly difficult to implement efficiently because most of its expressions have all sorts of different meanings that involve all sorts of different executions that are not distinguished by any syntactic or type annotation. The common intuition is that only JIT compilers can handle it efficiently because they can rely on heuristic-based strategies that require having the program and the data on hand. But static (AOT) compilers can speculate and use heuristics too! To demonstrate that, we propose Hopc, an AOT compiler for JavaScript, based on the following assumption: The most likely data structure a program will use is the one for which the compiler is able to produce its best code. Thus, contrary to most AOT compilers, Hopc does not rely on complex static analyses to optimize programs. It simply tries to generate its best code that it protects with guards. In this lecture, we will first present the basic techniques for compiling classical dynamically typed functional programming such as Scheme, and then, once that sets, we will dig into the specificities of the compilation of modern dynamic languages such as JavaScript.
Programming Language Foundations in Agda
Phil Wadler
The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs. Accordingly, the title of this course also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes. The textbook for the course is a literate Agda script, freely available online at https://plfa.inf.ed.ac.uk.