LIVE
Introduction to the PhD
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
- try Agda
- try Erlang (done)
- try Smalltalk (in progress)
- try Elixir
- try Celluloid
- try Rubinius
- try ACL2
- adapt OpenSCAD to be able to construct objects line by line like with CoqIde
- look at Paral ITP (done)
- look at TeXmacs
- try Omniscient Debugging
- look at User Interfaces for Theorem Provers meetings (in progress)
- look at Computer Aided Verification conference (in progress)
- look at MetaML (in progress)
- look at JetBrain's
- loot at Multi-stage Programming (in progress)
- try the Clay generic language (in progress)
Readings
- Preliminary Design of the SAFE Platform (done)
- Mostly-Automated Verification of Low-Level Programs (in progress)
- A Tactic Language for the System Coq (in progress)
- Proof style (done)
- coq-tutorial-ml-tactics (todo)
- An abstract type for constructing tactics in Coq (in progress)
- Notions of Computation and Monads (todo)
- Contextual Modal Type Theory (todo)
- On the expressive power of schemes (in progress)
- HOL-light's tutorial (in progress)
- Three Years of Experience with Sledgehammer (todo)
- SSReflect (in progress)
- Locally nameless representation (todo)
- The PoplMark Challenge (in progress)
- Program Verification Through Characteristic Formulae (todo)
- Asynchronous Proof Processing with Isabelle/Scala (todo)
- Isabelle/Isar - A versatile environment for humans (todo)
- Verified Just-In-Time Compiler on x86 (todo)
- CRML (in progress)
- A logic for duck typing (todo)
- Creating Languages in Racket (todo)
- Open, extensible composition models (todo)
- Bidirectional Type Checking (todo)
- From Type Checking by Recursive Descent to Type Checking with an Abstract Machine (todo)
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)
What is a type checker with parallelism ?
…
- …