ROADMAP 830 Bytes
Newer Older
MARCHE Claude's avatar
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 8
* tools: WhyML (JC), IDE (Claude)
* semantics:
MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
* 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 ==

* Builtin arrays in provers (Francois)
26 27
(done) make install 
(done) debug "make -j" 
MARCHE Claude's avatar
MARCHE Claude committed
28 29 30 31 32
* META for ocamlfind
* headers



MARCHE Claude's avatar
docs  
MARCHE Claude committed
33 34


MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38 39
= Roadmap for 2011 =

* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
MARCHE Claude committed
40
* Coq realizations of theories
MARCHE Claude's avatar
MARCHE Claude committed
41

MARCHE Claude's avatar
docs  
MARCHE Claude committed
42 43 44 45



= Papers to write =
MARCHE Claude's avatar
MARCHE Claude committed
46 47 48 49 50 51 52 53

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