Commit 10f8d879 authored by MARCHE Claude's avatar MARCHE Claude

roadmap

parent 73d0b5b2
......@@ -5,12 +5,19 @@
== long-term projects ==
* entiers machines
* modules, raffinement (these de Leon)
* support for higher-order
* extraction, more generally how to turn Why3 into a real programming language (these de Martin)
* rapprocher la logique et les programmes
** variant dans la logique ?
** monter les fonctions de programmes pures dans la logique ?
* internal interpreter, test of specifications, quickcheck
* BWare project, support for rewrite rules, improved support for provers,
......@@ -22,6 +29,8 @@
** support efficace des invariants de données
** développer des composants réutilisables prouvés.
* jessie3
== Papers to write ==
* paper on the module system, its semantics, realizations, avec en
......@@ -142,6 +151,8 @@ Scheduled for 31 october 2013
* input language
** lemma functions
** polymorphic recursion permitted
** types "opaques" ???
* new provers:
** veriT 201310
......@@ -308,6 +319,8 @@ Scheduled for 31 october 2013
** Metitarski TODO: improve it (CLAUDE, GUILLAUME)
** others ?
* simplification de (a && false) ne devrait pas etre false
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment