This paper presents the verification of a generational copying garbage collector for the
CakeML runtime system. The proof is split into an algorithm proof and an implementation …

Decomposing the design (or documentation) of large systems is a practical necessity but
finding compositional development methods for concurrent software is technically …

In computer science community, garbage collection is a dynamic storage management
technology to ensure the reliability of computer systems. In this paper, we consider two …

Garbage collectors (GCs) were invented as a technique to free programmers from the
tedious and error-prone task of manual memory management. Traditionally, tracing …

The OCaml programming language finds application across diverse domains, including
systems programming, web development, scientific computing, formal verification, and …

Modern compilers are complex programs, performing several heuristic-based optimisations.
As such, and despite extensive testing, they may contain bugs leading to the introduction of …

In the computer science community, garbage collection is a dynamic storage management
technology to ensure the reliability of computer systems. In this paper, we consider two …

Compiling concurrent and managed languages involves implementing sophisticated
interactions between client code and the runtime system. An emblematic runtime service …

Résumé Abstract Les compilateurs modernes constituent des programmes complexes,
réalisant de nombreuses optimisations afin d'améliorer la performance du code généré. Du …

Modern compilers for concurrent, managed languages involve sophisticated interactions
between the client code and the runtime system. An emblematic runtime service, whose …