Publications

2022

1. A Conceptual Framework for Safe Object Initialization: A Principled and Mechanized Soundness Proof of the Celsius Model

   Blaudeau, Clément, and Liu, Fengyun

   Proc. ACM Program. Lang., vol. 6, Oct, 2022

   [Abs] [URL] [DOI]

   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.

2021

1. OCaml modules: formalization, insights and improvements

   Blaudeau, Clément

   Master's thesis, École polytechnique fédérale de Lausanne, pp. 67, Sep, 2021

   [PDF] [URL]

2020

1. A Verified Packrat Parser Interpreter for Parsing Expression Grammars

   Blaudeau, Clement, and Shankar, Natarajan

   In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 3–17, 2020

   [Abs] [URL] [DOI]

   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.