helm/papers/calculemus-2003/outline.txt

   1 1) Introduzione
   2   - web services
   3   - monet
   4   - svariati WS per CAS e TP
   5   - proof assistant
   6     - bassa automazione
   7     - application centric no client/server
   8     ==>> proof assistants come WS client
   9   - omega ants
  10 2) Architettura
  11   - figura 7.1 mia tesi
  12   - attori (client, broker, tutor)
  13     - ruoli e funzionalita' di ognuno di essi (breve)
  14   - mapping con gli attori di monet
  15 3) Dettagli
  16   3.1) codifica dello stato e dei suggerimenti
  17     - oss: l'architettura e' generica non dipenda da una particolare codifica di
  18       dimostrazioni
  19     - interfaccia verso il broker
  20   3.2) client
  21     - proof assistant
  22   3.3) broker
  23     - registri
  24     - interfaccia verso i client (registrazione, sottoscrizione, state change,
  25       deregistrazione)
  26     - interfaccia verso i tutor (registrazione, suggerimento, deregistrazione)
  27   3.4) tutor
  28     - cosa puo' implementare un tutor
  29     - nessuna assunzione sulla correttezza del suggerimento
  30     - interfaccia verso il broker (start/stop musing)
  31     - thread (?)
  32 4) Sample session
  33   - screen shot
  34 5) Tutor implementati
  35   - stupidi
  36     - (1-1) con le tattiche del proof assistant
  37     - generazione automatica
  38   - searchPatternApply
  39 6) Conclusioni e sviluppi futuri
  40   - success story (gTopLevel)
  41     - tattiche pesanti
  42     ==>> distribuzione
  43     - scelta troppo larga per i neofiti
  44     ==>> suggerimenti
  45   - utile per power user (distribuzione)
  46   - utili per newbie (apprendimento)
  47   - sviluppi futuri
  48     - recursion?
  49     - rating dei risultati
  50     - risposte negative (disabilitare tattiche)
  51     - blackboard?
  52     - GUI
  53     - descrizione monet