PhD

September 2012 to September 2015

With Yann Régis-Gianas and Hugo Herbelin.

The goal is to turn Coq into an efficient and impure programming language, without scarifying the safety of its kernel. Coq should replace OCaml, C# and more.

We firstly focused on decision procedures for the Cybele project. We now work on adding effects to Coq.

A draft of the PhD is available here, and ongoing experiments published here.

Where

I work in the Pir2 team of Inria and Université Paris 7, mostly with Yann Régis-Gianas, Lourdes del Carmen González Huesca and Pierre-Marie Pédrot.

Timeline

The weeks are not always representative of real weeks but stand for units of work.

Week ω

TODO

Week 32 – 04/21/13

TODO
  • make the Coq version of SmartPrint observationally purely functional
  • release the extracted code as a new version of SmartPrint

Week 31 – 04/14/13

TODO

The goal is to do as much as possible by one week to get a usable release and move on.

  • read A modular module system
  • use explicative warnings instead of errors
  • have a good part of the standard OCaml library
  • handle the functors
  • add run methods for the effects in Coq
  • run the test suite to see if it behaves as the Coq code
  • add extraction for the effects
  • add the extraction step to the test suite
  • specialize the standard library to extract back the same OCaml functions
  • test the extraction of SmartPrint

Week 30 – 04/07/13

  • compile the let rec and construct
  • compile the OCaml's List module (without comparison functions)
  • show that the sorting function cannot raise exception
TODO
  • certify the sorting functions
  • handle the functors
  • compile the Map and Set modules

Week 29 – 03/31/14

DONE
  • add a basic support of inequalities
  • change the IO effect to have (possibly finite) streams
  • add an annotation mechanism to choose if recursive functions use the non-termination monad
  • add an environment for type variables
  • compile the OCaml's List module without sorting and comparison functions
TODO
  • implement the libraries Buffer, List and String
  • use explicative warnings instead of errors
  • compile the let rec and construct

Week 28 – 12/23/13 to 03/24/14

  • many improvements of CoqOfOCaml (mainly: effects support)

Week 27 – 12/16/13

Week 26 – 12/09/13

Week 25 – 12/02/13

Week 24 – 11/25/13

  • PPrint library used for pretty-printing
  • effects using monads (a lot of flood)

Week 23 – 11/18/13

  • support of records and modules in CoqOfOCaml
  • typed OCaml AST extracted from the .cmt files

Week 22 – 11/11/13

Week 21 – 10/21/13

TODO

Week 20 – 10/14/13

  • reading of Verifying Higher-order Programs with the Dijkstra Monad: they verify 3,000 lines of JavaScript with higher-order functions and states importing it to F*. This tool generates first-order verification conditions handled by Z3. A Dijkstra monad is a state monad annotated by a weakest-precondition predicate transformer. It may be better to have just predicates instead of predicate transformers. There is one big monad handling a state represented by a heap, exceptions and monotonicity properties. For simpler cases, like purely functional programs, they add a property enforcing the fact that the state is not modified. They also talk about permissions system for references and dynamic typing to import JavaScript. Unfortunately, some typing rules had to be added to F* in order to type monadic programs (the F* type system seems already quite complex).
  • survey of Rust: they have four kinds of pointers. This separation is based on a lot of experience writing the Firefox's web render in C++. They say owning pointers and borrowed are enough in most cases. We should focus on them to start with.
  • survey of ATS: an ML-like language with dependent and linear types. I would say it has the same goal as us (programming with dependent types and effects) but extending ML instead of extending Coq. As a result the proving part is not as evolved as in Coq, and effects are not properly typed (a function can just be pure or not pure). However they have a lot of examples, including concurrent programs, and can interact with C libraries.
  • quick reading of Verifying Stateful Programs with Substructural State and Hoare Types: a functional language FX with a simple form of dependent types and linear types to handle mutable states. Compiled to proof carrying .Net assemblies.
  • quick reading of L³ : A Linear Language with Locations: an ML-like language which references can be safely updated to a value of another type
  • quick reading of The Spec# Programming System: An Overview: a safer extension to C#, adding easy to use yet practical features. There are non-null references, pre and post-conditions, exceptions which can be raised, ... It is compiled to .Net assemblies and Boogie.

Week 19 – 10/07/13

  • thinking about reification of effects in Gallina for plumbery
TODO

Week 18 – 09/30/13

Week 17 – 09/23/13

  • reading of The type and effect discipline (Jean-Pierre Talpin and Pierre Jouvelot): a type and effects inference system with regions for an ML-like language with references
  • partial reading of the PhD of Jean-Christophe Filliâtre: Preuve de programmes impératifs en théorie des types: similar to our work. I would say that the main difference is in the approach: in this PhD, Coq is only used to encode the semantic and prove properties. For us, Coq is also the source programming language.
  • idea of a declaration mechanism for effects

Week 16 – 09/16/13

  • some thoughts about a GMP example

Week 15 – 09/09/13

Week 14 – 09/02/13

  • restarting of the PhD after holidays
  • website Coq.io to centralize the PhD's production
  • some experiments about a package manager for Coq

Week 13

TODO

Week 12

Week 11

  • reading of Pretty-big-step semantics: a simplest definition of big-step semantics, mainly to handle nicely exceptions and non-termination. Still more complex to me than monads in a complete language.
  • reading of Operational Semantics Using the Partiality Monad: definition of big-step semantics using monads for partiality and non-termination, with a proven correct toy compiler in Agda. The co-inductive monad may not be necessary (the inductive nat → option α is enough). The simulation relation with the virtual machine is complex too.
  • reading of Coinductive big-step operational semantics

Week 10

  • beginning of a compiler of arithmetic expressions with assertions to typed assembly
  • paper accepted at ESEC/FSE 2013 about probabilistic programs (from a previous internship at Microsoft India)

Week 9

Week 8

TODO

Week 7

  • thinking about the specification of effects (traces are probably the most general method)
  • thinking about inference of effects using the existing unification and dependent types mechanism in Coq (works for some restricted cases, but hard to generalize)
  • partial reading of Modular compilers based on monad transformers

Week 6

  • thinking about a monad-like system for effects with effects which can be combined in a commutative manner; look at implicit-monads on GitHub
  • attending to the TYPES 2013 conference

Week 5

TODO

Week 4

  • make a blog for PPS
  • prepare slides for Cybele

Week 3

  • idea of a certified extraction process from Coq to a monadic Coq to remove the proof terms from decision algorithms
  • idea of a JIT'd x86 DSL in Coq to give to Coq access to the computational efficiency of a real Turing computer
  • beginning of an extraction plugin

Week 2

  • github repository for Cybele
  • abstract to submit to TYPES checked
  • evaluation of performances of a congruence version returning booleans
  • CICM conference checked
TODO
  • congruence example in a proof by certificate manner (we got an universe inconsistency)
  • SAT solver
  • registers allocation checker

Week 1

Readings

Partiality and Recursion in Interactive Theorem Provers — An Overview
Journal article about the main ways to define recursive functions in Coq.
A Coinductive Monad for Prop-Bounded Recursion
Coinductive bind and return connectors to define a non-termination monad. Nice theory but slow to use. Possibility to pause the computations and continue.
Reflecting Proofs in First-Order Logic with Equality
Reflexive proofs for first-order logic using traces generated by CiME.
Verifying an algorithm computing Discrete Vector Fields for digital imaging
Interesting formalization of an algorithm for computer vision. They first write an Haskell program, test it with QuickCheck and convert it by hand to Coq. The resulting procedure has only a termination proof to type-check. We could probably simplify this kind of development using our monad.
Validating register allocation and spilling
Soudness by "translation validation" of the register allocation of Compcert. An allocation is proven correct a posteriori by guessing the allocation scheme. About 350 lines for the validator, 900 for its correctness. Compile-time overhead of 20 %. Can work with different allocation strategies.

TODO