Indagini in Deep Inference

La tesi è uno studio di alcuni aspetti della nuova metodologia “deep inference”, abbinato ad una rivisitazione dei concetti classici di proof theory, con l'aggiunta di alcuni risultati originali orientati ad una maggior comprensione dell'argomento, nonché alle applicazioni pratiche. Nel primo capitolo vengono introdotti, seguendo un approccio di stampo formalista (con alcuni spunti personali), i concetti base della teoria della dimostrazione strutturale – cioè quella che usa strumenti combinatoriali (o “finitistici”) per studiare le proprietà delle dimostrazioni. Il secondo capitolo focalizza l'attenzione sulla logica classica proposizionale, prima introducendo il calcolo dei sequenti e dimostrando il Gentzen Hauptsatz, per passare poi al calcolo delle strutture (sistema SKS), dimostrando anche per esso un teorema di eliminazione del taglio, appositamente adattato dall'autore. Infine si discute e dimostra la proprietà di località per il sistema SKS. Un percorso analogo viene tracciato dal terzo ed ultimo capitolo, per quanto riguarda la logica lineare. Viene definito e motivato il calcolo dei sequenti lineari, e si discute del suo corrispettivo nel calcolo delle strutture. L'attenzione qui è rivolta maggiormente al problema di definire operatori non-commutativi, che mettono i sistemi in forte relazione con le algebre di processo.

DTCU: Alberi Decisionali per la Classificazione di Dati Incerti

Oggi piu' che mai e' fondamentale essere in grado di estrarre informazioni rilevanti e conoscenza dal grande numero di dati che ci possono arrivare da svariati contesti, come database collegati a satelliti e sensori automatici, repository generati dagli utenti e data warehouse di grandi compagnie. Una delle sfide attuali riguarda lo sviluppo di tecniche di data mining per la gestione dell’incertezza. L’obiettivo di questa tesi e' di estendere le attuali tecniche di gestione dell’incertezza, in particolare riguardanti la classificazione tramite alberi decisionali, in maniera tale da poter gestire incertezza anche sull’attributo di classe.

Una realizzazione distribuita di test neuropsicologici

Questa tesi fornisce una realizzazione di alcuni test neuropsicologici, scelti in collaborazione di un neuropsicologo, che cercano di sostituire foglio e penna con touch screen e dita. L'obiettivo è quello di ricreare il test senza aggiungere agenti esterni derivanti dalla nuova interfaccia, per far sì che la fruizione del test sia buona almeno quanto quella del corrispettivo non digitale. Il risultato finale dovrebbe apportare dei vantaggi sostanziali al processo di somministrazione di questi test.

Rassegna dei framework per lo sviluppo di applicazioni mobili

Lo stato attuale del mercato continua a dimostrare come l'interesse del pubblico verso i dispositivi mobili sia in costante crescita; se fino a pochi anni fa il termine smartphone era ai piu' privo di significato, ora e' abbastanza comune per giovani e adulti essere concentrati su piccoli dispositivi dove si possono contattare i clienti via e-mail, verificare lo stato di avanzamento dei processi aziendali, consultare il web e cosi' via. L'obiettivo di questa tesi e' introdurre l'utilizzo di diverse tipologie di framework, prendendo come riferimento i sistemi operativi per i dispositivi mobili e quello di presentare soluzioni (attraverso i framework) per lo sviluppo di applicazioni mobili su diverse piattaforme software.

Una semantica distribuita per il Multi-CCS utilizzando reti di Petri

Questa tesi descrive e approfondisce l'algebra di processo Multi-CCS, le fornisce una semantica basata sulle reti di Petri non limitate - a correzione e miglioramento della precedente - e una dimostrazione dettagliata della sua correttezza, ovvero della bisimilitudine tra la marcatura ottenuta dalla uova semantica e da un generico processo Multi-CCS e lo stesso processo nella semantica di default definita sugli LTS

Ottimalità dell'ottimalità - Complessità della riduzione su grafi di condivisione

Trent’anni or sono il concetto di ottimalità venne formulato in senso teorico da Lévy, ma solo un decennio dopo Lamping riesce a darne elegante implementazione algoritmica. Realizza un sistema di riduzione su grafi che si scoprirà poi avere interessanti analogie con la logica lineare presentata nello stesso periodo da Girard. Ma l’ottimalità è davvero ottimale? In altre parole, l’implementazione ottimale del λ calcolo realizzata attraverso i grafi di condivisione, è davvero la migliore strategia di riduzione, in termini di complessità? Dopo anni di infondati dubbi e di immeritato oblìo, alla conferenza LICS del 2007, Baillot, Coppola e Dal Lago, danno una prima risposta positiva, seppur parziale. Considerano infatti il caso particolare delle logiche affini elementare e leggera, che possiedono interessanti proprietà a livello di complessità intrinseca e semplificano l’arduo problema. La prima parte di questa tesi presenta, in sintesi, la teoria dell’ottimalità e la sua implementazione condivisa. La seconda parte affronta il tema della sua complessità, a cominciare da una panoramica dei più importanti risultati ad essa legati. La successiva introduzione alle logiche affini, e alle relative caratteristiche, costituisce la necessaria premessa ai due capitoli successivi, che presentano una dimostrazione alternativa ed originale degli ultimi risultati basati appunto su EAL e LAL. Nel primo dei due capitoli viene definito un sistema intermedio fra le reti di prova delle logiche e la riduzione dei grafi, nel secondo sono dimostrate correttezza ed ottimalità dell’implementazione condivisa per mezzo di una simulazione. Lungo la trattazione sono offerti alcuni spunti di riflessione sulla dinamica interna della β riduzione riduzione e sui suoi legami con le reti di prova della logica lineare.

Studio e sviluppo di un'applicazione mobile per iOS nell'ambito della BI: un task manager per SAP Business Planning and Consolidation

La tesi riguarda lo sviluppo di un'applicazione che estende la possibilità di effettuare i caricamenti dei package di SAP BPC ai dispositivi mobile, fino ad ora questo era possibile solo attraverso l'interfaccia di Microsoft Excel.

Analisi statica dei Deadlock in Featherweight Java con Futuri

Abbiamo studiato ABSFJf, un linguaggio ad oggetti concorrente con tipi di dato futuro ed operazioni per acquisire e rilasciare il controllo delle risorse. I programmi ABSFJf possono manifestare lock (deadlock e livelock) a causa degli errori del programmatore. Per individuare staticamente possibili com- portamenti non voluti abbiamo studiato e implementato una tecnica per l'analisi dei lock basata sui contratti, che sono una descrizione astratta del comportamento dei metodi. I contratti si utilizzano per formare un automa i cui stati racchiudono informazioni di dipendenza di tipo chiamante-chiamato; vengono derivati automaticamente da un algoritmo di type inference e model- lati da un analizzatore che sfrutta la tecnica del punto

Migration strategies from IPv4 to IPv6 in a complex service provider environment

Progettazione ed implementazione di una strategia di migrazione da IPv4 a IPv6 in una realtà complessa come quella del consorzio interuniversitario CINECA. Sono stati presi in considerazione sia i livelli di rete e trasporto, sia il livello applicativo, cercando di fornire una visione completa delle problematiche incontrate. La strategia di migrazione scelta comprende le scelte tecniche fino ad ora implementate dal CINECA e i successivi passi che verranno intrapresi in futuro.