ROADMAP

= Roadmap for December 2010 =

== Documentation ==

1 Introduction (TODO: a finir)
2 Syntax, tutorial: JCF + Andrei3
3 IDE (Claude)
4 Standard lib of theories: TODO
* semantics:
* tutorial for API:
** build a task (done)
** call a prover (done) 
** apply a transformation (TODO)
** develop a new transformation (TODO)
* API: Andrei + Francois

== IDE ==

(Claude)

* database, session save and restore (done)
* Coq output (done)
* Gappa output (done)
* debug hide goals (TODO)
* add "context" options (TODO)
* add transf "inline goal" (TODO)
* add button "remove" (TODO)
* add button "replay" (TODO)

== Misc ==

* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)

* option -version a tous les executables + affichage dans l'IDE (TODO)
* Builtin arrays in provers (TODO: Francois)
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
* META for ocamlfind (TODO: Francois)
* headers (done)








= Roadmap for 2011 =

* WhyML (JC) 
* Jessie3
* traceability
* Coq plugin
* Coq realizations of theories




= Papers to write =

* Encodings and transformations (Andrei+Francois, CADE 2011, deadline January 2011)
* Caml code ?
* logic language for talking to provers
** FOL + poly + alg + ind + rec ? + theories
* VACID-0
* system description (e.g. at CAD, TACAS)
* rapports recherche ?