ML 2022
who it's for
OCaml developers, compiler engineers, language researchers, runtime systems engineers, language tool developers, formal verification engineers, FFI and bindings developers
topics
boxroot caller-roots protocol; per-domain root pools for OCaml 5; match compiler decision trees; unboxed types and layout lattice; tagged integer techniques (sofa, Reno); property-based tests extracted from F*; OCaml GADT to Coq translation; offshoring mutable binding translation; module shapes metadata for tooling; interpreter generation from skeletal semantics; strong call-by-need module reduction; algebraic subtyping for extensible records
| title | author | length |
|---|---|---|
| Boxroot, fast movable GC roots for a better FFI | Guillaume Munch-Maccagnoni, Gabriel Scherer | 15m |
Boxroot is a C library that implements a caller-roots protocol and an allocator for one-word roots, used already by several OCaml–Rust bindings. It chooses… | ||
| A New Match Compiler for Standard ML of New Jersey | David MacQueen | 17m |
Replaces a 30‑year‑old match compiler with a reimplementation that builds an and/or tree, extracts a decision tree via an ordered frontier worklist, then emits… | ||
| Unboxed types for OCaml | Richard A. Eisenberg, Stephen Dolan, Leo White | 17m |
Proposal adds unboxed types to OCaml to eliminate pointer boxing and heavy allocation (example: a pair of 32-bit ints on 64-bit needing many words and… | ||
| What About the Integer Numbers? | Daan Leijen | 16m |
Argues for fast hardware support for proper integers and presents three novel tricks for tagged integers, including the sofa technique that performs a… | ||
| Verify, but test: extracting property-based tests from F* specifications | Antonio Locascio, Germán Andrés Delbianco, Marco Stronati | 14m |
Extracts F pre and postconditions into OCaml Boolean predicates via a tiny Meta F tactic and runs them as QCheck tests against production data. Targets an… | ||
| Interpreting OCaml GADTs into Coq | Jacques Garrigue, Takafumi Saikawa | 19m |
Implements a two-pronged translation that maps OCaml GADT indices to an intensional ML-type syntax and then interprets those into concrete Coq types so… | ||
| Do Mutable Variables Have Reference Types? | Oleg Kiselyov | 14m |
Offshoring fails for mutable variables: naive translation that treats OCaml refs as C pointers either forces ad hoc restrictions (refs only for base types… | ||
| Module Shapes for Modern Tooling | Thomas Refis, Ulysse Gérard, Leo White | 16m |
Adds a compact language called Shapes to the OCaml compiler that represents module structure and tracks definitions through functor application, includes… | ||
| Necro ML: Generating OCaml Interpreters | Louis Noizet, Alan Schmitt | 14m |
Necro ML generates OCaml interpreters from skel skeletal semantics and outputs modular, monad-parameterized code that preserves unspecified types and terms. A… | ||
| An OCaml use case for strong call-by-need reduction | Gabriel Scherer, Nathanaëlle Courant | 21m |
Describes a concrete OCaml-compiler change: a strong call-by-need reduction strategy for the module language, implemented as an evaluator inside the compiler… | ||
| Towards Algebraic Subtyping for Extensible Records | Rodrigo Marques, Mario Florido, Pedro Vasconcelos | 16m |
Extends Simple-sub to support extensible records by adding row variables to the type language and a concrete row expansion step in the constraint solver… | ||
| The Ultimate Conditional Syntax | Lionel Parreaux | 16m |
Claims that a generalized if-expression called the Ultimate Conditional Syntax subsumes ML pattern matching and is implemented in MLscript, using nested… | ||
| Efficient and Scalable Parallel Functional Programming Through Disentanglement | Sam Westrick | 48m |
Claims a practical system that exploits a memory property called disentanglement by partitioning memory into a tree of heaps so task-local allocations and… | ||
| nothing matches | ||