Extending Implicit Computational Complexity and Abstract Machines to Languages with Control

The Curry-Howard isomorphism is the idea that proofs in natural deduction can be put in correspondence with lambda terms in such a way that this correspondence is preserved by normalization. The concept can be extended from Intuitionistic Logic to other systems, such as Linear Logic. One of the nice conseguences of this isomorphism is that we can reason about functional programs with formal tools which are typical of proof systems: such analysis can also include quantitative qualities of programs, such as the number of steps it takes to terminate. Another is the possiblity to describe the execution of these programs in terms of abstract machines. In 1990 Griffin proved that the correspondence can be extended to Classical Logic and control operators. That is, Classical Logic adds the possiblity to manipulate continuations. In this thesis we see how the things we described above work in this larger context.

Vending Machines avanzate basate su principi di Physical Web e Internet of Things

La costante evoluzione tecnologica sta portando alla luce nuove possibilità, che un tempo non erano nemmeno immaginabili. Uno dei settori che si è rivoluzionato maggiormente negli ultimi anni è quello delle telecomunicazioni e questo ha portato sia a una riduzione dei costi per le connessioni a Internet, sia ad un aumento delle loro capacità e prestazioni; di conseguenza queste connessioni sono diventate più accessibili e affidabili permettendo alle persone e alle cose di accedere a Internet quasi ininterrottamente. Questo sviluppo sta portando innumerevoli benefici, ma come ciascuna innovazione tecnologica, tuttavia, i benefici si accompagnano a nuove sfide. In questo elaborato viene dapprima analizzato lo stato dell’arte, i benefici, le problematiche e gli attuali interessi da parte di alcuni dei maggiori player verso l’Internet of Things. Vengono poi prese in considerazione due problematiche: l'individuazione e l'interazione con gli oggetti connessi a Internet, portando come esempio l'utilizzo e la ricerca di una vending machine, un distributore automatico. Proponendo una soluzione, in primo luogo è stato effettuato lo sviluppo di un ecosistema che sfrutta le potenzialità del Physical Web, implementando ad hoc ogni componente, dall'emissione del beacon Eddystone-URL alla visualizzazione della pagina ad esso associata. In secondo luogo questa è stata creata un'applicazione Android che sfrutta l'altro tipo di frame offerto dalla piattaforma beacon di Google, l'Eddystone-UID. Queste due applicazioni vengono quindi analizzate e messe a confronto, per individuare i punti forti e le mancanze delle rispettive piattaforme.