ROADMAP 1.2 KB
Newer Older
MARCHE Claude's avatar
roadmap  
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
roadmap  
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
roadmap  
MARCHE Claude committed
17 18 19 20 21

== IDE ==

(Claude)

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

== Misc ==

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

MARCHE Claude's avatar
MARCHE Claude committed
37
* Builtin arrays in provers (TODO: Francois)
MARCHE Claude's avatar
MARCHE Claude committed
38 39 40
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
MARCHE Claude's avatar
MARCHE Claude committed
41 42
* META for ocamlfind (TODO: Francois)
* headers (done)
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
43 44 45



MARCHE Claude's avatar
docs  
MARCHE Claude committed
46 47


MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
48 49
= Roadmap for 2011 =

MARCHE Claude's avatar
MARCHE Claude committed
50
* WhyML (JC) 
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
51 52 53
* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
claude  
MARCHE Claude committed
54
* Coq realizations of theories
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
55

MARCHE Claude's avatar
docs  
MARCHE Claude committed
56 57 58 59



= Papers to write =
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
60 61 62 63 64 65 66 67

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