Papers

Flambda 2 is an IR and optimisation pass for OCaml centred around inlining. We discuss the engineering constraints that shaped it and the overall structure that allows the compiler to be fast enough to handle very large industrial code bases.

In this talk, we will present an overview of the abstract domains that drive the Flambda 2 optimiser for OCaml programs. Like most optimising compilers, Flambda 2 relies on static analysis to find optimisation opportunities. There are several different analyses that are actually performed. Here we will focus on a forward value analysis that we call Flambda 2 Types. Despite its name, it fits quite well the definition of an abstract domain (in the sense of abstract interpretation), and it is through that angle that we will introduce it.

In this presentation, we will explore the compilation of garbage-collected languages, such as Java or OCaml, to WebAssembly (Wasm). The limitations of JavaScript as the web’s default language led to the development of Wasm, a secure and predictable-performance modular language. However, compiling garbage-collected languages to Wasm presents challenges, including the need to compile or re-implement the runtime and difficulties in transferring verified properties. Various techniques for representing values in memory are discussed, with a focus on OCaml’s approach. An extension called Wasm-GC is introduced, enabling the compilation of garbage-collected languages to Wasm by incorporating features like `int31` and garbage-collected structs. The paper presents Wasocaml, a complete OCaml compiler for Wasm-GC, and discusses benchmarks and future work in compiling garbage-collected languages to WebAssembly.

Opam 1.2 was released in 2014. It was four years before opam 2.0 succeeded it, and another three for opam 2.1. The release of opam 2.2 is imminent and will have arrived just a year after its predecessor. This talk presents features added to opam 2.1 intended to make dealing with multiple versions of opam easier. We see how small additional metadata, both stored in `.opam` “roots” and also added to opam’s command line to provide opam’s developers with the chance to add new features more easily, with confidence that users will be able to upgrade safely. In presenting this, we’ll also trumpet some of what we think are the amazing new features of opam 2.1 (and 2.2) and why we think you should keenly watch for new releases and upgrade immediately on release!

User-defined effects and effect handlers are advertised and advocated as a relatively easy-to-understand and modular approach to delimited control. They offer the ability of suspending and resuming a computation and allow information to be transmitted both ways between the computation, which requests a certain service, and the handler, which provides this service. Yet, a key question remains, to this day, largely unanswered: how does one modularly specify and verify programs in the presence of both user-defined effect handlers and primitive effects, such as heap-allocated mutable state? We answer this question by presenting a Separation Logic with built-in support for effect handlers, both shallow and deep. The specification of a program fragment includes a protocol that describes the effects that the program may perform as well as the replies that it can expect to receive. The logic allows local reasoning via a frame rule and a bind rule. It is based on Iris and inherits all of its advanced features, including support for higher-order functions, user-defined ghost state, and invariants. We illustrate its power via several case studies, including (1) a generic formulation of control inversion, which turns a producer that ``pushes'' elements towards a consumer into a producer from which one can ``pull'' elements on demand, and (2) a simple system for cooperative concurrency, where several threads execute concurrently, can spawn new threads, and communicate via promises.

In this talk, we will introduce a new tool called digodoc, that builds a graph of an opam switch, associating files, libraries, and opam packages into a cyclic graph of inclusions and dependencies. We will then explain how we used that tool to build a documentation website that displays the generated documentation of a large set of opam packages from the official opam repository. Thanks to digodoc, users can easily navigate between module documentations, sources, packages, and libraries. We think it is an interesting contribution to the OCaml ecosystem.

We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and the weak memory model.

Effect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads, and coroutines to be composably expressed. We present a design and evaluate a full-fledged efficient implementation of effect handlers for OCaml, an industrial-strength multi-paradigm programming language. Our implementation strives to maintain the backwards compatibility and performance profile of existing OCaml code. Retrofitting effect handlers onto OCaml is challenging since OCaml does not currently have any non-local control flow mechanisms other than exceptions. Our implementation of effect handlers for OCaml: (i) imposes a mean 1% overhead on a comprehensive macro benchmark suite that does not use effect handlers; (ii) remains compatible with program analysis tools that inspect the stack; and (iii) is efficient for new code that makes use of effect handlers.

In this talk, we will present `opam-bin`, an opam plugin that builds binary opam packages on the fly to speed-up reinstallation of packages. `opam-bin` also creates opam repositories for these binary packages in order to make them easy to share with other users. We will show how it works and how to use it on a daily basis.

In this talk we present our work on a syntax definition for the OCaml language in the syntax definition formalism SDF3. SDF3 supports high-level definition of concrete and abstract syntax through declarative disambiguation and definition of constructors, enabling a direct mapping to abstract syntax. Based on the SDF3 syntax definition, the Spoofax language workbench produces a complete syntax aware editor with a parser, syntax checking, parse error recovery, syntax highlighting, formatting with correct parenthesis insertion, and syntactic completion. The syntax definition should provide a good basis for experiments with the design of OCaml and the development of further tooling. In the talk we will highlight interesting aspects the syntax definition, discuss issues we encountered in the syntax of OCaml, and demonstrate the editor.

Since their inception state-machine frameworks have proven their worth by finding defects in everything from the underlying AUTOSAR components of Volvo cars to digital invoicing sys- tems. These case studies were carried out with Erlang’s commercial QuickCheck state-machine framework from Quviq, but such frameworks are now also available for Haskell, F#, Scala, Elixir, Java, etc. We present a typed state-machine framework for OCaml based on the QCheck library and illustrate a number concepts common to all such frameworks: state modeling, commands, interpreting commands, preconditions, and agreement checking.

AD-OCaml is a library framework for calculating mathematically exact derivatives and deep power series approximations of almost arbitrary OCaml programs via algorithmic differentiation. Unlike similar frameworks, this includes programs with side effects, aliasing, and programs with nested derivative operators. The framework also offers implicit parallelisation of both user programs and their transformations. The presentation will provide a short introduction to the mathematical problem, the difficulties of implementing a solution, the design of the library, and a demonstration of its capabilities.

In this talk we describe our experience in using an automatic API-migration strategy dedicated at changing the signatures of OCaml functions, using the Rotor refactoring tool for OCaml. We perform a case study on open source Jane Street libraries by using Rotor to refactor comparison functions so that they return a more precise variant type rather than an integer. We discuss the difficulties of refactoring the Jane Street code base, which makes extensive use of PPX macros, and ongoing work implementing new refactorings.

Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code? To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing nonatomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model. We illustrate this claim via a number of case studies: we verify several implementations of locks with respect to a classic, memory-model-independent specification. Thus, a coarse-grained application that uses locks as the sole means of synchronisation can be verified in the Concurrent-Separation-Logic fragment of Cosmo, without any knowledge of the weak memory model.

Irmin is an OCaml library for building distributed databases with the same design principles as Git. Existing Git users will find many familiar features: branching/merging, immutable causal history for all changes, and the ability to restore to any previous state. Irmin v2 adds new accessibility methods to the store: we can now use Irmin from a CLI, or in a browser using `irmin-graphql`. It also has a new backend, `irmin-pack`, which is optimised for space usage and is used by the Tezos blockchain.

LexiFi maintains an OCaml compiler extension that enables introspection through runtime type representations. Recently, we implemented a syntax extension (PPX) that enables the use of LexiFi runtime types on vanilla compilers. We propose to present our publicly available runtime types and their features. Most notably, we want to present a mechanism for pattern matching on runtime types with holes.

SmartPy is a complete system to develop smart-contracts for the Tezos blockchain. It is an embedded EDSL in Python to write contracts and their tests scenarios. It includes an online IDE, a chain explorer, and a command line interface. Python is used to generate programs in an imperative, type inferred, intermediate language called SmartML. SmartML is also the name of the OCaml library which provides an interpreter, a compiler to Michelson (the smart-contract language of Tezos), as well as a scenario “on-chain” interpreter. The IDE uses a mix of OCaml built with `js_of_ocaml` and pure Javascript. The command line interface also builds with `js_of_ocaml` to run on Node.js.

OCaml-CI is a CI service for OCaml projects. It uses metadata from the project’s opam and `dune` files to work out what to build, and it uses caching to make builds fast. It automatically tests projects against multiple OCaml versions and OS platforms. The CI has been deployed on around 50 projects so far on GitHub, and many of them see response times an order of magnitude quicker than with less integrated CI solutions. This talk will introduce the CI service and then look at some of the technologies used to build it.

With the availability of multicore variants of the recent OCaml versions (4.10 and 4.11) that maintain backwards compatibility with the existing OCaml C-API, there has been increasing interest in the wider OCaml community for parallelising existing OCaml code.

`odoc` is the latest attempt at creating a documentation tool which handles the full complexity of the OCaml language. It has been a long time coming as tackling both the module system and rendering into rich documents makes for a difficult task. Nevertheless we believe the two recent developments provides the final pieces of the OCaml documentation puzzle. This two improvements split `odoc` in two layers: a model layer, with a deep understanding of the module system, and a document layer allowing for easy definition of new outputs.

This proposal describes a presentation to be given at the OCaml’20 workshop. The presentation will cover a new OCaml filesystem, ImpFS, and the related libraries. The filesystem makes use of a B-tree library presented at OCaml’17 and a key-value store presented at ML’19. In addition, there are a number of other support libraries that may be of interest to the community. ImpFS represents a single point in the filesystem design space, but we hope that the libraries we have developed will enable others to build further filesystems with novel features.

Coda is a new cryptocurrency that uses zk-SNARKs to dramatically reduce the size of data needed by nodes running its protocol. Nodes communicate in a format automatically derived from type definitions in OCaml source files. As the Coda software evolves, these formats for sent data may change. We wish to allow nodes running older versions of the software to communicate with newer versions. To achieve that, we identify stable types that must not change over time, so that their serialisations also do not change.

In this article, we share our experience in prototyping chemoinformatics and structural bioinformatics software in OCaml

We propose a harmonious extension of OCaml's `open` construct. OCaml's existing construct `open M` imports the names exported by the module `M` into the current scope. At present `M` is required to be the path to a module. We propose extending `open` to instead accept an arbitrary module expression, making it possible to succinctly address a number of existing scope-related difficulties that arise when writing OCaml programs.

We propose a new semantics for shared-memory parallel programs that gives strong guarantees even in the presence of data races. Our local data race freedom property guar- antees that all data-race-free portions of programs exhibit sequential semantics. We provide a straightforward oper- ational semantics and an equivalent axiomatic model, and evaluate an implementation for the OCaml programming language. Our evaluation demonstrates that it is possible to balance a comprehensible memory model with a reasonable (no overhead on x86, ~0.6% on ARM) sequential performance trade-off in a mainstream programming language

We propose a memory model for OCaml, broadly following the design of axiomatic memory models for languages such as C++ and Java, but with a number of differences to provide stronger guarantees and easier reasoning to the programmer, at the expense of not admitting every possible optimisation.

The language Eff is an OCaml-like language serving as a prototype implementation of the theory of algebraic effects, intended for experimentation with algebraic effects on a large scale. We present the embedding of Eff into OCaml, using the library of delimited continuations or the Multicore OCaml branch. We demonstrate the correctness of the embedding denotationally, relying on the tagless-final-style interpreter-based denotational semantics, including the novel, direct denotational semantics of multi-prompt delimited control. The embedding is systematic, lightweight, performant, and supports even higher-order, 'dynamic' effects with their polymorphism. OCaml thus may be regarded as another implementation of Eff, broadening the scope and appeal of that language.

We present Learn OCaml, a Web application that packs a set of learning activities for people who want to learn OCaml. It includes an integrated and reworked version of the venerable Try OCaml and an exercise environment with automated grading derived from the one developed for the OCaml MOOC. It works entirely in the browser, the server being used for storing static files and synchronising between different devices. A special effort has been made to make it usable on tablets and even mobiles. A main public instance will be hosted at OCamlPro, but the project is open-source, and universities can host their own version on site. We will also provide a public repository for teachers to contribute lessons and exercises.

Louis Gesbert covers the current state of the OCaml Platform in September 2016. Introducing the game-changing integrations to opam 2.0, the roadmap, and many more an aspects of the OCaml Platform as a whole like `opam-publish`.

We present an ongoing project at OCamlPro, the development of a semantic analyser of OCaml code based on abstract interpretation techniques. This analysis relies on the presence of the whole program at compile time, it should work on full actual programs and shows interesting promises in terms of uncaught exceptions detection.

In this talk, we will present a starting project at OCamlPro, the development of a debugging framework for OCaml native-code applications, based on the LLDB Debugger, a debugger built on top of the LLVM framework. We implemented a complete binding of LLDB C++ API for OCaml, and then used it to build several tools, one "generic" debugger, and two small utilities to monitor the memory behavior of OCaml applications.

We present a work-in-progress about adding namespaces to OCaml. Inspired by other languages such as Scala or C++, our aim is to design and formalise a simple and non-intrusive namespace mechanism without complexifying the core language. Namespaces in our approach are a simple way to define libraries while avoiding name clashes. They are also meant to simplify the build process, clarifying and reducing (to zero whenever possible) the responsibility of external tools.

The OCaml Platform combines the OCaml compiler toolchain with a coherent set of tools for build, documentation, testing, and IDE integration. The project is a collaborative effort across the OCaml community, tied together by the OCaml Labs group in Cambridge and with other major contributors listed above. The requirements of the Platform are being guided by the industrial OCaml Consortium (primarily Jane Street, Citrix, and Lexifi). This talk follows up the OCaml 2013 talk that introduced the Platform. Since then, many tools have been released in parallel via the opam package manager, and this year’s talk will demonstrate the concrete workflow that ties them together (see Figure 2). We will first recap the Platform ethos briefly, update on the opam package manager v1.2 and conclude with the Platform workflow.

I spend a lot of time hacking the OCaml compiler. Hence when I write some code, I have a good glimpse of what the generated assembly will look like. This is nice when I want to write performance sensitive code, but as I usually write code for which execution time doesn't matter much, this mainly tends to torture me. A small voice in my head is telling me "you shouldn't write it like that, you known you could avoid this allocation." And usually, following that indication would only tend to make the code less readable. But there is a solution to calm that voice\: making the compiler smarter than me. OCaml compilation mechanisms are quite predictable. There is no dark magic to replace your ugly code by a well-behaving one, but it always generates reasonably efficient code. This is a good thing in general, as you won't be surprised by code running more slowly than what you usually expect. But it does not behave very well with dumb code. This may not often seem like a problem with code written by humans, but generated code, for example coming from camlp4/ppx, or compiled from another language to OCaml, may fall into that category. In fact, there is another common source for non-human written code: inlining.

OCamlot provides a distributed, continuous testing service for opam package quality and compatibility. Using signals from GitHub, OCamlot ensures that, before being merged, patches submitted to the opam repository are thoroughly tested on the variety of supported configurations, architectures, and systems. The resulting improved build and metadata quality in turn speeds up development on other aspects of the Platform through earlier error feedback. A high-quality package repository is also very important for new user retention.

In this paper, we present the current state of our work on profiling the memory usage of OCaml programs. Our technique allows to observe track types, allocation points, and reachability paths of blocks with no runtime cost, except for saving the observations.

One year after the foundation of OCamlPro, Fabrice Le Fessant presents at the OCaml Workshop a brief summary of the tasks undertaken in the span of that fateful year. Cheat Sheets, opam package manager, and many more are the start of a long stream of contributions for the OCaml Distribution and Community at large.

A two-fold presentation covering both a study of OCaml programs' memory behaviour and the development of memory profiling tools that were on-going at OCamlPro at the time. These works aimed at decreasing memory footprint, pinpoint and fix memory leaks, and decrease the amount of time spent in memory management at runtime.

Six months after the start of the development of the opam package manager, Frederick Tuong, Fabrice Le Fessant, and Thomas Gazagnaire present for the first time what would in time become the official package manager for the OCaml Distribution. Covering the current state of the repository, and future prospects for the platform, this small piece of media witholds a significant piece of history for OCaml.

Why the next language you learn should be functional.

Meta-programming tutorial with Camlp4

In this talk, we will firstly describe the architecture of XenServer and the XenAPI and discuss the challenges faced with implementing an Objective Caml based solution. These challenges range from the low-level concerns of interfacing with Xen and the Linux kernel, to the high-level algorithmic problems such as distributed failure planning. In addition, we will discuss the challenges imposed by using OCaml in a commercial environment, such as supporting product upgrades, enhancing supportability, and scaling the development team.

This book chapter gives an in-depth abstract of the Core ML type system, with an emphasis on type inference. The type inference algorithm is described as the composition of a constraint generator, which produces a system of type equations, and a constraint solver, which is presented as a set of rewrite rules.

This paper explains why it is sound to generalise certain type variables at a `let` binding, even when the expression that is being `let`-bound is not a value. This relaxed version of Wright's classic “value restriction” was introduced in OCaml 3.07.

This paper provides more details about the technical machinery behind polymorphic variants, focusing on the rules for typechecking deep pattern matching constructs.

This note describes the experimental recursive modules introduced in OCaml 3.07.

This paper explains most of the typechecking machinery behind polymorphic variants. At its heart is an extension of Core ML's type discipline with so-called local constraints.

This paper offers a dynamic semantics, a static semantics, and a compilation scheme for OCaml's labeled and optional function parameters.

All you ever wanted to know about the garbage collector found in Caml Light and OCaml's runtime system.

This accessible paper describes a simplified implementation of the OCaml module system, emphasizing the fact that the module system is largely independent of the underlying core language. This is a good tutorial to learn both how modules can be used and how they are typechecked.

This short paper explains how to design a modular, extensible interpreter using polymorphic variants.

This paper proposes a device for re-introducing first-class polymorphic values into ML while preserving its type inference mechanism. This technology underlies OCaml's polymorphic methods.

This paper provides theoretical foundations for OCaml's object-oriented layer, including dynamic and static semantics.

This paper briefly explains what polymorphic variants are about and how they are compiled.

This paper surveys and compares several data representation strategies, including the one used in the OCaml native-code compiler.

This work extends the above paper by introducing so-called applicative functors, that is, functors that produce compatible abstract types when applied to provably equal arguments. Applicative functors are also a feature of OCaml.

All you ever wanted to know about the garbage collector found in Caml Light and OCaml's runtime system.

This paper describes the semantics and the type system of Core ML and uses a simple syntactic technique to prove that well-typed programs cannot go wrong.

This paper presents a variant of the Standard ML module system that introduces a strict distinction between abstract and manifest types. The latter are types whose definitions explicitly appear as part of a module interface. This proposal is meant to retain most of the expressive power of the Standard ML module system, while providing much better support for separate compilation. This work sets the formal bases for OCaml's module system.

This paper describes a concurrent version of the garbage collector found in Caml Light and OCaml's runtime system.

Superseded by "Portable, Unobtrusive Garbage Collection for Multiprocessor Systems"

This report contains a abstract of the ZINC compiler, which later evolved into Caml Light, then into OCaml. Large parts of this report are out of date, but it is still valuable as a abstract of the abstract machine used in Caml Light and (with some further simplifications and speed improvements) in OCaml.