ROADMAP 956 Bytes
Newer Older
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
1
2
3
4
5
6

= Roadmap for December 2010 =

== Documentation ==

* API: Andrei + Francois
MARCHE Claude's avatar
MARCHE Claude committed
7
* tools: IDE (Claude)
MARCHE Claude's avatar
MARCHE Claude committed
8
* semantics:
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
* tutorial for API:
** build a task
** call a prover
** apply a transformation
** develop a new transformation

== IDE ==

(Claude)

* database, session save and restore
* Coq output
* Gappa output

== Misc ==

MARCHE Claude's avatar
MARCHE Claude committed
25
26
27
28
29
* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
30
* Builtin arrays in provers (Francois)
MARCHE Claude's avatar
MARCHE Claude committed
31
32
33
34
35
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
* META for ocamlfind (TODO: ?)
* headers (TODO: ?)
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
36
37
38



MARCHE Claude's avatar
docs    
MARCHE Claude committed
39
40


MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
41
42
= Roadmap for 2011 =

MARCHE Claude's avatar
MARCHE Claude committed
43
* WhyML (JC) 
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
44
45
46
* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
claude    
MARCHE Claude committed
47
* Coq realizations of theories
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
48

MARCHE Claude's avatar
docs    
MARCHE Claude committed
49
50
51
52



= Papers to write =
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
53
54
55
56
57
58
59
60

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