*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.

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.

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

- look at the Eff language (Bower, Pretwar), the Frank language (McBride), Hancock and Setzer (handlers, interfaces), Edwin Brady (algebraic effects and dependent types), Plotkin (algebraic effects), call by push-value (Paul Levy)
- read about typed assembly languages: From System F to Typed Assembly Language, A Dependently Typed Assembly Language
- look at the Disciplined Disciple Compiler project
- read Linear maps (Shuvendu Lahiri)

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

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

- compile the
`let rec and`

construct - compile the OCaml's List module (without comparison functions)
- show that the sorting function cannot raise exception

- certify the sorting functions
- handle the functors
- compile the Map and Set modules

- 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

- implement the libraries Buffer, List and String
- use explicative warnings instead of errors
- compile the
`let rec and`

construct

- many improvements of CoqOfOCaml (mainly: effects support)

- SmartPrint released on OPAM

- better version of SmartPrint

- project SmartPrint for a new pretty-printing library in OCaml
- port of CoqOfOCaml to SmartPrint

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

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

- beginning of a compiler of OCaml to Coq: GitHub page

- look at Mezzo
- read Intuitionistic Refinement Calculus
- look at the Lambda-Mu-Nu Calculus

- 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.

- thinking about reification of effects in Gallina for plumbery

- look at Hs to Gallina
- look at the Habit language
- look at Single Assignment C

- partial reading of the PhD of Sylvain Lebresne Une approche de la détection statique d'exceptions non rattrapées en appel par nom: not directly useful since we focus on call-by-value instead of call-by-name.
- make cheat sheets to teach the C language
- plugin with a declaration mechanism for effects: sources
- ideas about an attributes (examples in .Net) and a meta-operators system for Coq terms

- 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

- some thoughts about a GMP example

- trip to Venice for the birthday of Pierre-Louis Currien
- online OPAM repository with the
`trunk`

contribs

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

- read Formalizing the LLVM Intermediate Representation for Verified Program Transformations (Steve Zdancewic)

- reading of Certified Software (Zhong Shao)
- reading of Certificate translation for optimizing compilers (Gilles Barthe)
- reading of A formally verified compiler back-end (Xavier Leroy, Sandrine Blazy)
- reading of the LLVM's IR language
- reading of Compiling Functional Types to Relational Specifications for Low Level Imperative Code
- reading of A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language (Adam Chlipala)
- reading of A Verified Compiler for an Impure Functional Language (Adam Chlipala)
- reading of Formal verification of a C-like memory model and its uses for verifying program transformations (Xavier Leroy, Sandrine Blazy)
- partial reading of the PhD Certification of a Tool Chain for Deductive Program Verification (Paolo Herms)

- 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

- 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)

- summer school EJCP 2013 at Saint-Malo and Rennes (France)
- five minutes presentation of the PhD

- reading of The Implicit Calculus of Constructions
- reading of The Implicit Calculus of Constructions as a Programming Language with Dependent Types
- reading of The Rooster and the Syntactic Bracket
- beginning of a typed assembly with termination

- find a nice definition of effects at the programmer level, starting from the assembly semantics to find the "natural" one
- read Trace-based verification of imperative programs with I/O
- read Effective Interactive Proofs for Higher-Order Imperative Programs

- 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

- 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

- do a first post for the next PPS blog: Proof by extraction in Coq: a new approach
- add a repository on GitHub to publish experiments

- read Lightweight Monadic Programming in ML
- read Polymonads
- read Optimizing ML Using a Hierarchy of Monadic Types
- read Monad Transformers and Modular Interpreters
- check if implicit monads can be added using type classes

- 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

- github repository for Cybele
- abstract to submit to TYPES checked
- evaluation of performances of a congruence version returning booleans
- CICM conference checked

- congruence example in a proof by certificate manner (we got an
`universe inconsistency`

) - SAT solver
- registers allocation checker

- a website for Cybele
- the get started section

- 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.

- Iterated Register Coalescing
- Formal Verification of Coalescing Graph-Coloring Register Allocation
- SAT-MICRO: petit mais costaud !
- Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq (PhD)
- A Functional Specification of Effects (PhD)
- Vers une certification de l'extraction de Coq (PhD)
- Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq (PhD)