We present ZipML , a new path-based type system for a fully fledged ML-module language that avoids the signature avoidance problem. This is achieved by introducing floating fields , which act as additional fields of a signature, invisible to the user but still accessible to the typechecker. In practice, they are handled as zippers on signatures, and can be seen as a lightweight extension of existing signatures. Floating fields allow to delay the resolution of instances of the signature avoidance problem as long as possible or desired. Since they do not exist at runtime, they can be simplified along type equivalence, and dropped once they became unreachable. We give rewriting rules for the simplification of floating fields without loss of type-sharing and present an algorithm that implements them. Remaining floating fields may fully disappear at signature ascription, especially in the presence of toplevel interfaces. Residual unavoidable floating fields can be shown to the user as a last resort, improving the quality of error messages. Besides, ZipML implements early and lazy strengthening, as well as lazy inlining of definitions, preventing duplication of signatures inside the typechecker. The correctness of the type system is proved by elaboration into M ω , which has itself been proved sound by translation to F ω . ZipML has been designed to be an improvement over OCaml that could be retrofitted into the existing implementation.

ML modules come as an additional layer on top of a core language to offer large-scale notions of composition and abstraction. They largely contributed to the success of OCaml and SML. While modules are easy to write for common cases, their advanced use may become tricky. Additionally, despite a long line of works, their meta-theory remains difficult to comprehend, with involved soundness proofs. In fact, the module layer of OCaml does not currently have a formal specification and its implementation has some surprising behaviors. Building on previous translations from ML modules to Fω, we propose a type system, called Mω, that covers a large subset of OCaml modules, including both applicative and generative functors, and extended with transparent ascription. This system produces signatures in an OCaml-like syntax extended with Fω quantifiers. We provide a reverse translation from Mω signatures to path-based source signatures along with a characterization of signature avoidance cases, making Mω signatures well suited to serve as a new internal representation for a typechecker. The soundness of the type system is shown by elaboration in Fω. We improve over previous encodings of sealing within applicative functors, by the introduction of transparent existential types, a weaker form of existential types that can be lifted out of universal and arrow types. This shines a new light on the form of abstraction provided by applicative functors and brings their treatment much closer to those of generative functors.

An object under initialization does not fulfill its class specification yet and can be unsafe to use as it may have uninitialized fields. It can sometimes be useful to call methods on such a partially initialized object in order to compute a complex initial value, or to let the object escape its constructor in order to create mutually recursive objects. However, inadvertent usage of uninitialized fields can lead to run-time crashes. Those subtle programming errors are not statically detected by most modern compilers. While many other features of object-oriented programming languages have been thoroughly studied over the years, object initialization lacks a simple, systematic, and principled treatment. Building on the insights of previous work, we identify a set of four core principles for safe initialization: monotonicity, authority, stackability, and scopability. We capture the essence of the principles with a minimal calculus, Celsius, and show that the principles give rise to a practical initialization system that strikes a balance between expressiveness and simplicity. The meta-theory of the system is entirely mechanized using the Coq proof assistant. We believe that our approach based on well-identified core principles sheds new light on the underlying mechanisms ensuring safety and could serve as a basis for language design when faced with similar challenges.

Parsing expression grammars (PEGs) offer a natural opportunity for building verified parser interpreters based on higher-order parsing combinators. PEGs are expressive, unambiguous, and efficient to parse in a top-down recursive descent style. We use the rich type system of the PVS specification language and verification system to formalize the metatheory of PEGs and define a reference implementation of a recursive parser interpreter for PEGs. In order to ensure termination of parsing, we define a notion of a well-formed grammar. Rather than relying on an inductive definition of parsing, we use abstract syntax trees that represent the computational trace of the parser to provide an effective proof certificate for correct parsing and ensure that parsing properties including soundness and completeness are maintained. The correctness properties are embedded in the types of the operations so that the proofs can be easily constructed from local proof obligations. Building on the reference parser interpreter, we define a packrat parser interpreter as well as an extension that is capable of semantic interpretation. Both these parser interpreters are proved equivalent to the reference one. All of the parsers are executable. The proofs are formalized in mathematical terms so that similar parser interpreters can be defined in any specification language with a type system similar to PVS.