first checkin

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

diff --git a/helm/papers/calculemus-2003/outline.txt b/helm/papers/calculemus-2003/outline.txt
new file mode 100644 (file)
index 0000000..d349353
--- /dev/null
+++ b/helm/papers/calculemus-2003/outline.txt
@@ -0,0 +1,53 @@
+1) Introduzione
+  - web services
+  - monet
+  - svariati WS per CAS e TP
+  - proof assistant
+    - bassa automazione
+    - application centric no client/server
+    ==>> proof assistants come WS client
+  - omega ants
+2) 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
+  - screen shot
+5) Tutor implementati
+  - stupidi
+    - (1-1) con le tattiche del proof assistant
+    - generazione automatica
+  - searchPatternApply
+6) Conclusioni e sviluppi futuri
+  - success story (gTopLevel)
+    - tattiche pesanti
+    ==>> distribuzione
+    - scelta troppo larga per i neofiti
+    ==>> suggerimenti
+  - utile per power user (distribuzione)
+  - utili per newbie (apprendimento)
+  - sviluppi futuri
+    - recursion?
+    - rating dei risultati
+    - risposte negative (disabilitare tattiche)
+    - blackboard?
+    - GUI
+    - descrizione monet