ECTS - University of Pisa
Gli studenti dovranno acquisire solide basi di conoscenza circa i principi della semantica operazionale e denotazionale, le tecniche per relazionare l'una con l'altra nel caso di linguaggi imperativi e funzionali di ordine superiore. Inoltre dovranno familiarizzare con i principi della semantica operazionale e astratta per algebra di processi concorrenti, con lai logica temporale
L'esame scritto servirà a verificare che gli studenti abbiano compreso il materiale presentato durante il corso e che siano in grado di organizzare e strutturare i concetti appresi in efficaci risposte scritte.
Metodi di verifica:
Al termine del corso gli studenti dovrebbero essere in grado di dimostrare semplici proprietà formali di linguaggi e sistemi imperativi, dichiarativi, concorrenti In particolare dovrebbero essere in grado di applicare correttamente i più comuni principi di induzione e la teoria del punto fisso.
Esame scritto e orale.
Alla fine del corso gli studenti dovrebbero essere in grado di comprendere e applicare sistemi logici e definizioni induttive, di definire la semantica di linguaggi di programmazione, e di ragionare su eventuali equivalenze e corrispondenze tra specifiche astratte.
Non ci sono prerequisiti stringenti, ma ci si aspetta che gli studenti abbiano una buona familiarità con la matematica discreta, con le formule logiche del prim'ordine, con le grammatiche libere da contesto e siano in grado di comprendere frammenti di codice scritti in linguaggi imperativi.
Lezioni frontali e esercitazioni collettive.
Attività di apprendimento:
Frequenza: fortemente consigliata
Introduzione di tre modelli computazionali differenti e studio delle loro proprietà formali principali (imperativo: IMP, funzionale: HOFL, processi concorrenti: CCS) accompagnati da principi di induzione e da metodi di dimostrazione. Attivita' di laboratorio:
Testo principale:
Metodi di verifica:
