ROADMAP 1.44 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
* database, session save and restore (done)
* Coq output (done)
* Gappa output (done)
* debug hide goals (TODO)
26 27 28
* add "context" options (partially done)
** semantics not clear, should be clarified, documented and 
   implemented accordingly
MARCHE Claude's avatar
MARCHE Claude committed
29
* add transf "inline goal" (TODO)
30
** not urgent
MARCHE Claude's avatar
MARCHE Claude committed
31 32
* add button "remove" (TODO)
* add button "replay" (TODO)
33
** semantics: replay obsolete proofs
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
34 35 36

== Misc ==

MARCHE Claude's avatar
MARCHE Claude committed
37 38 39 40 41
* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)

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



MARCHE Claude's avatar
docs  
MARCHE Claude committed
52 53


MARCHE Claude's avatar
MARCHE Claude committed
54 55 56



MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
57 58
= Roadmap for 2011 =

MARCHE Claude's avatar
MARCHE Claude committed
59
* WhyML (JC) 
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
60 61 62
* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
claude  
MARCHE Claude committed
63
* Coq realizations of theories
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
64

MARCHE Claude's avatar
docs  
MARCHE Claude committed
65 66 67 68



= Papers to write =
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
69 70 71 72 73 74 75 76

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