ROADMAP 1.3 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5

= Roadmap for December 2010 =

== Documentation ==

MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9
1 Introduction (TODO: a finir)
2 Syntax, tutorial: JCF + Andrei3
3 IDE (Claude)
4 Standard lib of theories: TODO
MARCHE Claude's avatar
MARCHE Claude committed
10
* semantics:
MARCHE Claude's avatar
MARCHE Claude committed
11
* tutorial for API:
MARCHE Claude's avatar
MARCHE Claude committed
12 13 14 15 16
** build a task (done)
** call a prover (done) 
** apply a transformation (TODO)
** develop a new transformation (TODO)
* API: Andrei + Francois
MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20 21

== IDE ==

(Claude)

MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25
* database, session save and restore (done)
* Coq output (done)
* Gappa output (done)
* debug hide goals (TODO)
MARCHE Claude's avatar
MARCHE Claude committed
26
* add "context" options (TODO)
MARCHE Claude's avatar
MARCHE Claude committed
27 28 29
* add transf "inline goal" (TODO)
* add button "remove" (TODO)
* add button "replay" (TODO)
MARCHE Claude's avatar
MARCHE Claude committed
30 31 32

== Misc ==

MARCHE Claude's avatar
MARCHE Claude committed
33 34 35 36 37
* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)

MARCHE Claude's avatar
MARCHE Claude committed
38
* option -version a tous les executables + affichage dans l'IDE (TODO)
MARCHE Claude's avatar
MARCHE Claude committed
39
* Builtin arrays in provers (TODO: Francois)
MARCHE Claude's avatar
MARCHE Claude committed
40 41 42
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
MARCHE Claude's avatar
MARCHE Claude committed
43 44
* META for ocamlfind (TODO: Francois)
* headers (done)
MARCHE Claude's avatar
MARCHE Claude committed
45 46 47



MARCHE Claude's avatar
docs  
MARCHE Claude committed
48 49


MARCHE Claude's avatar
MARCHE Claude committed
50 51 52



MARCHE Claude's avatar
MARCHE Claude committed
53 54
= Roadmap for 2011 =

MARCHE Claude's avatar
MARCHE Claude committed
55
* WhyML (JC) 
MARCHE Claude's avatar
MARCHE Claude committed
56 57 58
* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
MARCHE Claude committed
59
* Coq realizations of theories
MARCHE Claude's avatar
MARCHE Claude committed
60

MARCHE Claude's avatar
docs  
MARCHE Claude committed
61 62 63 64



= Papers to write =
MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68 69 70 71 72

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