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 ?