ROADMAP 1.3 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)
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
roadmap  
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
roadmap  
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
roadmap  
MARCHE Claude committed
53
54
= Roadmap for 2011 =

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

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



= Papers to write =
MARCHE Claude's avatar
roadmap  
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 ?