Cari tutti,

il primo incontro del laboratorio in oggetto si terrà lunedì 2 ottobre dalle 16 alle 18 in aula M-Lab del polo Fibonacci. Il laboratorio proseguirà con cadenza settimanale, sempre nello stesso orario, e consterà di 10 incontri, più un intervento conclusivo (seminario di un esperto esterno) nella settimana 11-15 dicembre.

Alcune indicazioni pratiche: * è caldamente consigliato che portiate il vostro laptop, se ne avete uno, e che fin da ora proviate ad installare Lean 4 seguendo le istruzioni che trovate all'indirizzo https://leanprover-community.github.io/. Fate il possibile per ottenere un'installazione funzionante: in caso incontraste difficoltà insormontabili, il corso dovrebbe presto essere affiancato da tutor ai quali vi potrete rivolgere per aiuto tecnico. Vi daremo indicazioni più precise in merito al momento del primo incontro. * la prima lezione sarà principalmente un'introduzione teorica ai fondamenti logici del sistema. A partire dal secondo incontro contiamo di dedicare un'ampia fetta di tempo all'effettiva implementazione di dimostrazioni formali. * l'aula M è un laboratorio informatico: ci sembrava infatti opportuno che aveste a disposizione i computer di ateneo in caso non aveste un dispositivo personale. Le adesioni sono però state piuttosto numerose; valuteremo eventualmente in seguito al primo incontro la possibilità di spostarci in un'aula più capiente (che probabilmente non sarebbe un laboratorio, e richiederebbe quindi che abbiate tutti un laptop).

Cari saluti, Alessandro Iraci, Davide Lombardo, Marcello Mamino _______________________________________________ Utenti mailing list -- utenti@lists.dm.unipi.it To unsubscribe send an email to utenti-leave@lists.dm.unipi.it