Papers

With its strong academic roots, OCaml is known to be a spearhead in the development of Programming Language Theory. This page contains a selection of papers that have influenced OCaml and other functional programming languages.

Recommended Papers

Eff Directly in OCaml
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.
Oleg Kiselyov, KC Sivaramakrishnan
ocaml-workshop
core
language
A Memory Model for Multicore OCaml
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.
Stephen Dolan, KC Sivaramakrishnan
ocaml-workshop
multicore
Extending OCaml's `open`
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.
Runhang Li, Jeremy Yallop
ocaml-workshop
core
language
39 Papers
Title Years Tags Authors Actions
The ZINC Experiment, an Economical Implementation of the ML Language
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.
1990
compiler
runtime
Xavier Leroy Download PDF Download PostScript
A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML
Superseded by "Portable, Unobtrusive Garbage Collection for Multiprocessor Systems"
1993
garbage collection
runtime
Damien Doligez, Xavier Leroy Download PDF Download PostScript
A Syntactic Approach to Type Soundness
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.
1994
core
language
Andrew K. Wright, Matthias Felleisen Download PostScript
Manifest Types, Modules, and Separate Compilation
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.
1994
core
language
modules
Xavier Leroy Download PDF Download PostScript Download DVI
Portable, Unobtrusive Garbage Collection for Multiprocessor Systems
This paper describes a concurrent version of the garbage collector found in Caml Light and OCaml's runtime system.
1994
garbage collection
runtime
Damien Doligez, Georges Gonthier Download PDF Download PostScript
Applicative Functors and Fully Transparent Higher-Order Modules
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.
1995
core
language
modules
Xavier Leroy Download PDF Download PostScript Download DVI
Conception, Réalisation et Certification d'un Glaneur de Cellules Concurrent
All you ever wanted to know about the garbage collector found in Caml Light and OCaml's runtime system.
1995
garbage collection
runtime
Damien Doligez, Georges Gonthier Download PDF Download PostScript
The Effectiveness of Type-based Unboxing
This paper surveys and compares several data representation strategies, including the one used in the OCaml native-code compiler.
1997
compiler
runtime
Xavier Leroy Download PDF Download PostScript
Objective ML: An Effective Object-Oriented Extension to ML
This paper provides theoretical foundations for OCaml's object-oriented layer, including dynamic and static semantics.
1998
core
language
objects
Didier Rémy, Jérôme Vouillon Download PDF Download PostScript Download DVI
Programming with Polymorphic Variants
This paper briefly explains what polymorphic variants are about and how they are compiled.
1998
core
language
polymorphic variants
Jacques Garrigue Download PDF Download PostScript
Extending ML with Semi-Explicit Higher-Order Polymorphism
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.
1999
core
language
objects
Jacques Garrigue, Didier Rémy Download PDF Download PostScript Download DVI
A Modular Module 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.
2000
core
language
modules
Xavier Leroy Download PDF Download PostScript Download DVI
Code Reuse Through Polymorphic Variants
This short paper explains how to design a modular, extensible interpreter using polymorphic variants.
2000
core
language
polymorphic variants
Jacques Garrigue Download PostScript
Labeled and Optional Arguments for Objective Caml
This paper offers a dynamic semantics, a static semantics, and a compilation scheme for OCaml's labeled and optional function parameters.
2001
core
language
Jacques Garrigue Download PDF Download PostScript Download DVI
Optimizing Pattern Matching
All you ever wanted to know about the garbage collector found in Caml Light and OCaml's runtime system.
2001
pattern-matching
runtime
Fabrice Le Fessant, Luc Maranget View Online
Simple Type Inference for Structural Polymorphism
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.
2002
core
language
polymorphic variants
Jacques Garrigue Download PDF Download PostScript
A Proposal for Recursive Modules in Objective Caml
This note describes the experimental recursive modules introduced in OCaml 3.07.
2003
core
language
modules
Xavier Leroy Download PDF Download PostScript
Relaxing the Value Restriction
This paper explains why it is sound to generalize 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.
2004
core
language
Jacques Garrigue Download PDF Download PostScript
Typing Deep Pattern-matching in Presence of Polymorphic Variants
This paper provides more details about the technical machinery behind polymorphic variants, focusing on the rules for typechecking deep pattern matching constructs.
2004
core
language
polymorphic variants
Jacques Garrigue Download PDF Download PostScript
The Essence of ML Type Inference
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.
2005
core
language
François Pottier, Didier Rémy Download PostScript
Xen and the Art of OCaml
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.
2008
industrial
application
Anil Madhavapeddy Download PDF
Meta-Programming Tutorial with CamlP4
Meta-programming tutorial with Camlp4
2010
core
language
Jake Donham View Online
OCaml for the Masses
Why the next language you learn should be functional.
2011
industrial
Yaron Minsky View Online
Eff Directly in OCaml
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.
2016
ocaml-workshop
core
language
Oleg Kiselyov, KC Sivaramakrishnan Download PDF
A Memory Model for Multicore OCaml
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.
2017
ocaml-workshop
multicore
Stephen Dolan, KC Sivaramakrishnan Download PDF
Chemoinformatics and Structural Bioinformatics in OCaml
In this article, we share our experience in prototyping chemoinformatics and structural bioinformatics software in OCaml
2019
industrial
application
bioinformatics
François Berenger, Kam Y. J. Zhang, Yoshihiro Yamanishi View Online
Extending OCaml's `open`
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.
2019
ocaml-workshop
core
language
Runhang Li, Jeremy Yallop Download PDF
A Declarative Syntax Definition for OCaml
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.
2020
ocaml-workshop
Luis Eduardo de Souza Amorim, Eelco Visser View Online
A Simple State-Machine Framework for Property-Based Testing in OCaml
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.
2020
ocaml-workshop
Jan Midtgaard Download PDF
AD-OCaml: Algorithmic Differentiation for OCaml
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 parallelization 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.
2020
ocaml-workshop
Markus Mottl View Online
API Migration: Compare Transformed
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.
2020
ocaml-workshop
Joseph Harrison, Steven Varoumas, Simon Thompson, Reuben Rowe View Online Download PDF
Irmin v2
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.
2020
ocaml-workshop
Clément Pascutto, Ioana Cristescu, Craig Ferguson, Thomas Gazagnaire, Romain Liautaud View Online View Online
LexiFi Runtime Types
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.
2020
ocaml-workshop
Patrik Keller, Marc Lasson View Online Download PDF View Online
OCaml Under the Hood: SmartPy
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.
2020
ocaml-workshop
Sebastien Mondet View Online Download PDF
OCaml-CI: A Zero-Configuration CI
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 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.
2020
ocaml-workshop
Thomas Leonard, Craig Ferguson, Kate Deplaix, Magnus Skjegstad, Anil Madhavapeddy View Online
Parallelising Your OCaml Code with Multicore OCaml
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.
2020
ocaml-workshop
Sadiq Jaffer, Sudha Parimala, KC Sivaramarkrishnan, Tom Kelly, Anil Madhavapeddy Download PDF View Online
The Final Pieces of the OCaml Documentation Puzzle
`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.
2020
ocaml-workshop
Jonathan Ludlam, Gabriel Radanne, Leo White View Online
The ImpFS Filesystem
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.
2020
ocaml-workshop
Tom Ridge View Online
Types in Amber
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 serializations also do not change.
2020
ocaml-workshop
Paul Steckler, Matthew Ryan View Online