Object-oriented programs are often described as "models of the real world". Drawing on the work of Peirce, Sassure, Peter Bogh Anderson, and H. P. Lovecraft, I'll try and explain what this means and how it affects our programs and programming languages — functional, object-oriented, chthonic, or otherwise. I'll look at the relationships between simulation, programming, meta-programming, delegation, and inheritance. I'll try and justify the de-evolution from SIMULA to Smalltalk, Self, and Javascript. Finally I'll speculate about what it means when our programs don't just simulate the real world, but rise from the abyss replace it.

The Elm programming language pioneers the Model-View-Update (MVU) architecture for writing web applications in a functional style. Although popular amongst developers, MVU has not been studied formally; it is therefore difficult to reason about any extensions, and each implementer must re-discover the essence of the architecture.

We introduce lambda-mvu, a formal description of the MVU architecture as a concurrent lambda-calculus, and prove its correctness. We modularly extend lambda-mvu with subscriptions and commands as found in the Elm programming language. We then further extend the calculus with linearity and model transitions, which are sufficient to allow us to provide the first formal integration of session-typed communication in a GUI framework. We implement our approach in the Links tierless web programming language, and show examples including a two-factor authentication workflow and multi-room chat server.

Here are two trending topics in contemporary software development:

1. interactive notebook coding, e.g. Jupyter notebooks
2. multi-language projects, i.e. polyglot programming

This presentation examines the crossover between these two topics, and identifies a set of architectural design patterns that facilitate differing levels of programming language interoperability in such interactive environments. Health warning - this is work-in-progress ... or maybe work-about-to-start (?)

Telescopes give us composable contexts, but what if we could compose them more than one way?

I tried it, coupled it with an Information Aware presentation of type systems, and found a useful collection of tools to share. In particular, I derived a new representation for solving typechecking problems and a way to proceed from a type system to a logical specification of existing techniques suitable for checking dependently typed languages.

Aside from reading off implementations and verifying more complex ones, I hope this representation can also be used to discuss nuanced differences between systems and to explain the behaviour of typecheckers to users.

Slides

Multi-dimensional arrays play a major role in machine learning, numerical simulations or high-performance computing. Array programming in imperative languages involves explicit indexing within loop-nests which often leads to the code that is difficult to understand or reason about. APL offers a notation for array operations that is built around the notion of index-free combinators. APL programs are very concise yet carry very rich semantics. However, as APL is dynamically typed, reasoning about correctness of these programs is challenging.

Designing a type system for APL is even more challenging. First, the same operator has different behavior depending on the type and shape of its arguments. Secondly, the shape of the result of an operator typically depends on the shape of its arguments. Finally, the type of array elements may change at runtime.

In this talk I will describe preliminary results on formalising APL in Agda. I will present a shallow embedding of a core array language that makes it possible to define a set of APL operators and partially solve the overloading. As a result, a large set of APL programs can be translated into the proposed system. They can be then analysed for correctness or interpreted within Agda or compiled into executables.

A common practice in dependently typed programming is correct-by-construction programming — where we write programs that carry statically a lot of the information that is needed to verify them. For example, instead of having filter take a list of XS and produce a list of XS, we declare a property P and return, as well as the list of XS, a proof for each x in the returned list that it satisfies P. However, when we do correct-by-construction programming with fancy types, we sometimes lose sight of how these functions compute. In this talk, I rectify a long-standing bug in the Agda and Idris standard libraries in their definitions of Dec — the type family that captures the decidability of a proposition — so as to get back good computational properties.