X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fcalculemus-2003%2Foutline.txt;h=55cb826ce33af50f3ef36b9f7e15df33961a3940;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d349353faf95703ee23680f8fc2ddf4dcc766b8f;hpb=f59e3c55dde91612a2e8a16335f2a2e9137fde5f;p=helm.git diff --git a/helm/papers/calculemus-2003/outline.txt b/helm/papers/calculemus-2003/outline.txt index d349353fa..55cb826ce 100644 --- 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