A few papers on Caml

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 book chapter gives an in-depth description 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 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 Objective Caml 3.07.

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 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.

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 note describes the experimental recursive modules introduced in Objective Caml 3.07.

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

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 briefly explains what polymorphic variants are about and how they are compiled.

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

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 provides more details about the technical machinery behind polymorphic variants, focusing on the rules for typechecking deep pattern matching constructs.

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

This report contains a description 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 description of the abstract machine used in Caml Light and (with some further simplifications and speed improvements) in OCaml.

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

Superseded by the next paper.

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

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