ocaml 3.09 transition

[helm.git] / helm / papers / calculemus-2003 / outline.txt

diff --git a/helm/papers/calculemus-2003/outline.txt b/helm/papers/calculemus-2003/outline.txt
index d349353faf95703ee23680f8fc2ddf4dcc766b8f..55cb826ce33af50f3ef36b9f7e15df33961a3940 100644 (file)
--- a/helm/papers/calculemus-2003/outline.txt
+++ b/helm/papers/calculemus-2003/outline.txt
@@ -1,4 +1,5 @@
-1) Introduzione
+1) Zack, CSC
+ Introduzione
   - web services
   - monet
   - svariati WS per CAS e TP
@@ -7,31 +8,24 @@
     - application centric no client/server
     ==>> proof assistants come WS client
   - omega ants
-2) Architettura
+2) Zack
+  Architettura
   - figura 7.1 mia tesi
   - attori (client, broker, tutor)
     - ruoli e funzionalita' di ognuno di essi (breve)
   - mapping con gli attori di monet
-3) Dettagli
-  3.1) codifica dello stato e dei suggerimenti
-    - oss: l'architettura e' generica non dipenda da una particolare codifica di
-      dimostrazioni
-    - interfaccia verso il broker
-  3.2) client
-    - proof assistant
-  3.3) broker
-    - registri
-    - interfaccia verso i client (registrazione, sottoscrizione, state change,
-      deregistrazione)
-    - interfaccia verso i tutor (registrazione, suggerimento, deregistrazione)
-  3.4) tutor
-    - cosa puo' implementare un tutor
-    - nessuna assunzione sulla correttezza del suggerimento
-    - interfaccia verso il broker (start/stop musing)
-    - thread (?)
-4) Sample session
+3) Zack
+  Dettagli Implementativi
+  - codifica dello stato
+  - codifica dei suggerimenti
+  - registry del broker
+  - implementazione dei ws
+  - implementazione dei tutor (gen. automatica, thread)
+4) CSC
+   Sample session
   - screen shot
-5) Tutor implementati
+5) CSC
+    Tutor implementati
   - stupidi
     - (1-1) con le tattiche del proof assistant
     - generazione automatica
@@ -51,3 +45,4 @@
     - blackboard?
     - GUI
     - descrizione monet
+    - uso di Mathematical Object Manager