Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

Microscopic Modeling on complex networks

The field of complex systems is a growing body of knowledge, It can be applied to countless different topics, from physics to computer science, biology, information theory and sociology. The main focus of this work is the use of microscopic models to study the behavior of urban mobility, which characteristics make it a paradigmatic example of complexity. In particular, simulations are used to investigate phase changes in a finite size open Manhattan-like urban road network under different traffic conditions, in search for the parameters to identify phase transitions, equilibrium and non-equilibrium conditions . It is shown how the flow-density macroscopic fundamental diagram of the simulation shows,like real traffic, hysteresis behavior in the transition from the congested phase to the free flow phase, and how the different regimes can be identified studying the statistics of road occupancy.

Web advertising. Le comunicazioni commerciali on-line.

La tesi ha ad oggetto lo studio e l’approfondimento delle forme di promozione commerciale presenti in Rete caratterizzate, più che da una normale evoluzione, da continue metamorfosi che ridefiniscono ogni giorno il concetto di pubblicità. L’intento è quello di analizzare il quadro giuridico applicabile alla pubblicità via Web, a fronte della varità di forme e di modalità che essa può assumere. Nel lavoro vengono passate in rassegna le caratteristiche che differenziano la pubblicità commerciale on-line rispetto a quella tradizionale; tra le quali, particolare rilievo assume la capacità d’istaurare una relazione – diretta e non mediata – tra impresa e consumatore. Nel prosieguo viene affrontato il problema dell’individuazione, stante il carattere a-territoriale della Rete, della legge applicabile al web advertising, per poi passare ad una ricognizione delle norme europee ed italiane in materia, senza trascurare quelle emanate in sede di autodisciplina. Ampio spazio è dedicato, infine, all’esame delle diverse e più recenti tecniche di promozione pubblicitaria, di cui sono messi in evidenza gli aspetti tecnico-informatici, imprescindibili ai fini di una corretta valutazione del tema giuridico. In particolare, vengono approfonditi il servizio di posizionamento a pagamento offerto dai principali motori di ricerca (keywords advertising) e gli strumenti di tracciamento dei “comportamenti” on-line degli utenti, che consentono la realizzazione di campagne pubblicitarie mirate (on-line behavioural advertising). Il Web, infatti, non offre più soltanto la possibilità di superare barriere spaziali, linguistiche o temporali e di ampliare la propria sfera di notorietà, ma anche di raggiungere l’utente “interessato” e, pertanto, potenziale acquirente. Di queste nuove realtà pubblicitarie vengono vagliati gli aspetti più critici ed esaminata la disciplina giuridica eventualmente applicabile anche alla luce delle principali decisioni giurisprudenziali nazionali ed europee in materia, nonché delle esperienze giuridiche nord-americane e di tipo autoregolamentare.