Gradual Programming with Hedy and Creating Programming Languages in non-English
Verona: co-designing the type system, concurrency model, and runtime system
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
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
Programming Language Foundations in Agda
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.