programmare con un linguaggio funzionale a complessità polinomiale

Durante la programmazione di un eseguibile, di una funzione e pi?u in generale di qualsiasi software che richieda l'utilizzo per un certo tempo delle risorse di un calcolatore, uno degli aspetti fondamentali ?e lo studio del tempo di esecuzione. La conoscenza dei limiti sul tempo di esecuzione di un dato software permette una de?nizione, ad esempio, dei tempi necessari per giungere ad un certo risultato. La de?nizione di questo limite ha assunto negli anni molta importanza, ad esempio, nel caso dei sistemi di calcolo distribuiti, nei quali ?e di primaria importanza la conoscenza del limite del tempo di esecuzione a causa dell'utilizzo di macchine con risorse limitate. Negli ultimi anni si sta sviluppando un ramo della ricerca che ha come obiettivo la progettazione di sistemi di tipo che assegnano formule delle logiche leggere a lambda termini puri. In questi sistemi si pu?o de?nire un limite alla complessit?a di riduzione dei lambda termini tipabili. Poich?e il lambda calcolo pu?o essere inteso come il paradigma dei linguaggi di programmazione funzionale, risulta evidente come questi sistemi studiati per il lambda calcolo potranno essere estesi per i linguaggi di programmazione comunemente usati. Lo scopo del tirocinio ?e la realizzazione di un'IDE per programmare funzioni computabili in tempo polinomiale, usando uno di questi sistemi di assegnazione di tipo. Nel dettaglio ?e stato usato l'algoritmo di inferenza di tipo . Tale algoritmo inferisce tipi per lambda termini al secondo ordine, con la propriet?a che, se un termine possiede un tipo, allora la complessit?a della. sua valutazione ?e limitata da una funzione elementare nella lunghezza del termine. Il tirocinio si ?e svolto in diverse fasi. La prima parte di esso ?e consistita nel- lo studio dell'articolo \Light types for polynomial time computation in lambda calculus "di Patrick Baillot e Kazushige Terui[ref], successivamente \Veri?cation of Ptime reducibility for system F terms via Dual Light A?ne Logic "di Vincent Atassi, Patrick Baillot e Kazushige Terui[ref]. In seguito si ?e passati alla proget- tazione teorica del programma, con la de?nizione dei punti fondamentali del suo sviluppo. Dopo aver completato questa fase si ?e passati all'implementazione vera e propria del progetto. In?ne ?e stata svolta una fase di testing su di esso. Per la realizzazione del progetto ?e stato usato l'ambiente di sviluppo Eclipse e come linguaggio di programmazione Java. In particolare ?e stato usato Xtext che un plugin di Eclipse che facilita lo sviluppo di linguaggi di programmazione. Il progetto ?e stato sviluppato in ambiente Linux, ?e funziona correttamente per tale ambiente.