Package managers are legion. Every programming language and operating system has its own solution, each with subtly different semantics for dependency resolution. This fragmentation prevents multilingual projects from expressing precise dependencies across language ecosystems; it leaves external system dependencies implicit and unversioned; and it obscures the full dependency graph that supply-chain analysis depends on. We present the Package Calculus, a formalism for dependency resolution that unifies the core semantics of package managers. Through a series of formal reductions, we show how this core is expressive enough to model the diversity of real-world dependency expression languages. The calculus provides the theoretical foundation for future cross-ecosystem tooling, as a lingua franca of dependency expression.

Docker is a developer tool used by millions of developers to build, share and run software stacks. The Docker Desktop clients for Mac and Windows have long used a novel combination of virtualisation and OCaml unikernels to seamlessly run Linux containers on these non-Linux hosts. We reflect on a decade of shipping this functional OCaml code into production across hundreds of millions of developer desktops, and discuss the lessons learnt from our experiences in integrating OCaml deeply into the container architecture that now drives much of the global cloud. We conclude by observing just how good a fit for systems programming that the unikernel approach has been, particularly when combined with the OCaml module and type system.

When developing a new programming language, having a large corpus of both correct and incorrect programs allows language designers to test and explore the capabilities of their new language. However, bootstrapping such a corpus of incorrect programs is time-consuming and arduous. We therefore explore how to reuse code from more mature languages to generate a corpus of ill-typed code for newer ones. We have developed a compiler to Hazel, an emerging language with typed holes, from the more mature OCaml ecosystem. We find it practical to generate a comprehensive corpus of ill-typed programs for Hazel development, and discuss future larger scale efforts towards bridging ecosystems.

We explore how to provide programmers with an interactive interface for explaining the process by which static types and dynamic casts are derived, with the goal of improving the debugging of static and dynamic type errors. To this end, we define mathematical foundations for a decomposable highlighting system within a bidirectional system, and show how these can be propagated through dynamic types in a cast system. Our prototype implementation in the gradually typed Hazel language includes a web-based user interface, through which we highlight the importance of type level debugging.

We present Yirgacheffe, a declarative geospatial library that allows spatial algorithms to be implemented concisely, supports parallel execution, and avoids common errors by automatically handling data (large geospatial rasters) and resources (cores, memory, GPUs). Our primary user domain comprises ecologists, where a typical problem involves cleaning messy occurrence data, overlaying it over tiled rasters, combining layers, and deriving actionable insights from the results. We describe the successes of this approach towards driving key pipelines related to global biodiversity and describe the capability gaps that remain, hoping to motivate more research into geospatial domain-specific languages.

The proposed talk will outline the vision for a recently originated research project aiming to build a formally verified prototype of a foundational "operating system" for safeguarded AI, called Bastion, that grounds these activities within programming language theory, namely by combining dependent type theory (as a practical general-purpose theory of computational structures and proofs), Dijkstra monads (as a flexible formalism for reasoning about an AI agent's computational effects), and abstract types (for modularizing reasoningto individual components that can be separately developed by various stakeholders, including AI safety researchers, formal methods experts, organizations of various scales, and governments seeking to develop actionable, specific policy).

The current Internet architecture fails to treat the carbon emissions associated with networked services as a first-class metric. We propose extending the DNS with load balancing techniques to consider the carbon cost of scheduling decisions, and further to actively wake machines running networked services as a side effect of name resolution. By extending the DNS, we maintain compatibility with existing Internet infrastructure, unlocking the ability for existing applications to be carbon-aware.

Data-science is a vital tool in tackling the ongoing climate crisis, but it is one that has a significant cost to it also, in terms of energy used during execution and in terms of significant hardware investment required to run it. These are then amplified considerably in the exploratory nature of scientific research.We argue this is because the affordances of the operating system, particularly filesystems, make little effort to support reuse of computed artifacts directly or promote reuse through trusted lineage data. However, it turns out that many of the userspace interfaces exposed by the Linux kernel entirely support a radically more efficient -- a more frugal -- model of computation than is currently the default. In this talk, we explore a new OS architecture which defaults to deterministic, reusable computation with the careful recording of side effects. This in turn allows the OS to guide complex computations towards previously acquired intermediate results, but still allowing for recomputation when required. We use these interfaces to build a new Linux userspace where we put the workflow graph-containing relationships between tools, provenance and labelling-as the core of a system that drives how processes, data, and users interact. Our prototype shell, dubbed Shark, is a data-science first operating environment that is designed to both ensure efficient use of computation and storage resources, and to make it easy for non-experts to create pipeline descriptions from end results post-hoc. It does this by making the lineage graph of a data-pipeline the key concept that ties everything else together: by tracking how the data-pipeline evolves from experimental practice, and tracking what data has already been built and what hasn't we can prevent re-execution both at development and after publication.

In this talk we will explore: (i) how the conflicting incentives around carbon emissions reporting make existing systems unlikely to succeed; and (ii) how we could use ZKPs to allow for the accurate reporting of carbon claims without compromising on individual privacy and competitiveness requirements.

Eio provides an effects-based direct-style IO stack for OCaml 5. This talk introduces Eio's main features, such as use of effects, multicore support and lock-free data-structures, support for modular programming, interoperability with other concurrency libraries such as Lwt, Async and Domainslib, and interactive monitoring support enabled by the custom runtime events in OCaml 5.1. We will report on our experiences porting existing applications to Eio.

The upcoming 5.0 release of OCaml includes a new runtime tracing system designed for continuous monitoring of OCaml applications called Runtime Events. It enables very low overhead, programmatic access to performance data emitted by the OCaml runtime and garbage collector. This talk focuses on the implementation of Runtime Events and the user experience of writing applications exploiting this new feature.

Programming for the planet undoubtedly involves programming scientifically, but what kind of programming are we talking about and what makes it scientific? In what ways does it differ from other forms of programming, if at all? Is scientific programming, data science or machine learning fundamentally different to constructing a compiler or building a high-throughput web server? By considering how the scientific method (with its falsifiable hypotheses and repeatable and reproducible experiments) relates to scientific programming, I hope to explore how computer science and traditional programming techniques are coming up short in meeting the requirements of scientific programmers.

Carbon credits purchased in the voluntary carbon market allow unavoidable emissions, such as international flights for essential travel, to be offset by an equivalent climate benefit, such as avoiding emissions from tropical deforestation. However, many concerns regarding the credibility of these offsetting claims have been raised. Moreover, the credit market is manual, therefore inefficient and unscalable, and non-fungible, therefore illiquid. To address these issues, we propose an efficient digital methodology that combines remote sensing data, modern econometric techniques, and on-chain certification and trading to create a new digital carbon asset (the PACT stablecoin) against which carbon offsetting claims can be transparently verified. PACT stablecoins are produced as outputs from a reproducible computational pipeline for estimating the climate benefits of carbon offset projects that not only quantifies the CO2 emissions involved, but also allows for similar credits to be pooled based on their co-benefits such as biodiversity and jurisdictional attributes, increasing liquidity through fungibility within pools. We implement and evaluate the PACT carbon stablecoin on the Tezos blockchain, which is designed to facilitate low-cost transactions while minimizing environmental impact. Our implementation includes a contract for a registry for tracking issuance, ownership, and retirement of credits, and a custodian contract to bridge on-chain and off-chain transactions. Our work brings scale and trust to the voluntary carbon market by providing a transparent, scalable, and efficient framework for high-integrity carbon credit transactions.