helm/papers/calculemus-2003/outline.txt

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