Preparation to the PhD

Winter 2011

With Yann Régis-Gianas.

The main draft is available here (in French).

Goal

Make Coq more interactive using patchs and meta-languages. The proposal to get the grant is available here (in French).

Ideas

  • do a survey of the main tactic flavours (Coq, SSreflect, Mizard, …)
  • plug external tools to Coq to use a new tactic language (Ruby, …)
  • formalize what is a toplevel
  • formalize what is a debugger, the evaluation of a terms with holes
  • view type checking as abstract evaluation to formalize meta-languages
  • view patch type checking as abstract partial evaluation
  • study parallelism during type checking

TODO

Readings

Survey

The paper Proof style is already a good survey but needs to be updated (published in 1996).

Ruby plugin for Coq

Sources of the project are available here. It is not usable yet. The first step will be to be able to maipulate proof terms and make tactics on the Ruby side, before to connect it to Coq.

  • read DTD definition of Coq terms (done)
  • look at the Helm project (done)
  • look at the MoWGLI project (done)
  • define a class of terms and a printer to Coq (done)
  • define a toy set of tactics (done)
  • define goals with sub-goals (done)
  • define sum types with tactics (done)
  • manage equalities for simple proofs (done)
  • rewrite a new framework with better binders, goals with dependent holes (in progress)
  • look at Tac (todo)
  • show that they are more than two integers (todo)
  • give a general class for inductive types (todo)

What is a toplevel?

How to give a semantics to a toplevel given a semantics of a programming language, with a criteria for correctness? You can get the sources of a toy toplevel here.

  • define the semantic of a toplevel with respect to the semantic of a programming language (done)
  • use relations instead of partial functions (done)
  • explain what we want to modelize in the introduction (done)
  • give a simple example of a toplevel (done)
  • give an implementation of the toplevel (done)
  • add an undo command (done)

What is a debugger?

How to evaluate terms with holes or breakpoints?

  • extend the toplevel's theory with the "…" keyword and formalize it (done)
  • give an example of language with holes (done)
  • prove the correctness of the example (todo)
  • plug it to Gedit with a Python plugin (todo)
  • extend the semantic to a debugger (todo)
  • what does it mean to undo a command (todo)
  • what does it mean to undo a command when it is not possible and what can be preserved (todo)

What is a meta-language?

How to implement introspection and code generation with Smalltalk's style keeping static checkings?

  • view type checking as abstract evaluation (done)
  • formalize a meta-language with a semantics blended to type checking (done)
  • give examples (done)
  • use the object language as the meta-language (todo)
  • implement it (todo)
  • type code patches to type check in live (todo)

What is a patch type system?

What is the type of a code patch?

  • formalize a type-checker of a programming language with holes (in progress)