User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Gender equality and human development in Macedonia during transition (1991-2006)

The present thesis treats the issue of gender equality in Macedonia during the period of transition from the socialist system to the one of parliamentary democracy. The main aim is to mainstream the gender perspective in the analysis of the transitional policies through the examination of the basic citizenship rights to which citizens are entitled and by the means of the evaluation of their capabilities to exercise these rights. Gender equality, as one of the main strongholds of the concept of human development is measured through the application of nine gender relevant capabilities in a Case study conducted within selected municipalities in the country. Through the analysis of the Macedonian constitutional and legal framework and the assessment of gender based inequalities, the research questions the need for the enactment of a process of engendering of citizenship, which would integrate gender based differences, contemplate the private sphere of citizens lives and pledge participation in the political life of the country. The thesis, finally, analyses the gender equality strategy of the Macedonian government with the purpose to evaluate whether it is context based, i.e. it tackles the main fields where inequalities emerge and in this context whether it envisages a process of engendering of citizenship.

TCAD approaches to multidimensional simulation of advanced semiconductor devices

Technology scaling increasingly emphasizes complexity and non-ideality of the electrical behavior of semiconductor devices and boosts interest on alternatives to the conventional planar MOSFET architecture. TCAD simulation tools are fundamental to the analysis and development of new technology generations. However, the increasing device complexity is reflected in an augmented dimensionality of the problems to be solved. The trade-off between accuracy and computational cost of the simulation is especially influenced by domain discretization: mesh generation is therefore one of the most critical steps and automatic approaches are sought. Moreover, the problem size is further increased by process variations, calling for a statistical representation of the single device through an ensemble of microscopically different instances. The aim of this thesis is to present multi-disciplinary approaches to handle this increasing problem dimensionality in a numerical simulation perspective. The topic of mesh generation is tackled by presenting a new Wavelet-based Adaptive Method (WAM) for the automatic refinement of 2D and 3D domain discretizations. Multiresolution techniques and efficient signal processing algorithms are exploited to increase grid resolution in the domain regions where relevant physical phenomena take place. Moreover, the grid is dynamically adapted to follow solution changes produced by bias variations and quality criteria are imposed on the produced meshes. The further dimensionality increase due to variability in extremely scaled devices is considered with reference to two increasingly critical phenomena, namely line-edge roughness (LER) and random dopant fluctuations (RD). The impact of such phenomena on FinFET devices, which represent a promising alternative to planar CMOS technology, is estimated through 2D and 3D TCAD simulations and statistical tools, taking into account matching performance of single devices as well as basic circuit blocks such as SRAMs. Several process options are compared, including resist- and spacer-defined fin patterning as well as different doping profile definitions. Combining statistical simulations with experimental data, potentialities and shortcomings of the FinFET architecture are analyzed and useful design guidelines are provided, which boost feasibility of this technology for mainstream applications in sub-45 nm generation integrated circuits.

Costrutti ed Applicazioni di Programmazione Generica in Linguaggi Object-Oriented

Generic programming is likely to become a new challenge for a critical mass of developers. Therefore, it is crucial to refine the support for generic programming in mainstream Object-Oriented languages — both at the design and at the implementation level — as well as to suggest novel ways to exploit the additional degree of expressiveness made available by genericity. This study is meant to provide a contribution towards bringing Java genericity to a more mature stage with respect to mainstream programming practice, by increasing the effectiveness of its implementation, and by revealing its full expressive power in real world scenario. With respect to the current research setting, the main contribution of the thesis is twofold. First, we propose a revised implementation for Java generics that greatly increases the expressiveness of the Java platform by adding reification support for generic types. Secondly, we show how Java genericity can be leveraged in a real world case-study in the context of the multi-paradigm language integration. Several approaches have been proposed in order to overcome the lack of reification of generic types in the Java programming language. Existing approaches tackle the problem of reification of generic types by defining new translation techniques which would allow for a runtime representation of generics and wildcards. Unfortunately most approaches suffer from several problems: heterogeneous translations are known to be problematic when considering reification of generic methods and wildcards. On the other hand, more sophisticated techniques requiring changes in the Java runtime, supports reified generics through a true language extension (where clauses) so that backward compatibility is compromised. In this thesis we develop a sophisticated type-passing technique for addressing the problem of reification of generic types in the Java programming language; this approach — first pioneered by the so called EGO translator — is here turned into a full-blown solution which reifies generic types inside the Java Virtual Machine (JVM) itself, thus overcoming both performance penalties and compatibility issues of the original EGO translator. Java-Prolog integration Integrating Object-Oriented and declarative programming has been the subject of several researches and corresponding technologies. Such proposals come in two flavours, either attempting at joining the two paradigms, or simply providing an interface library for accessing Prolog declarative features from a mainstream Object-Oriented languages such as Java. Both solutions have however drawbacks: in the case of hybrid languages featuring both Object-Oriented and logic traits, such resulting language is typically too complex, thus making mainstream application development an harder task; in the case of library-based integration approaches there is no true language integration, and some “boilerplate code” has to be implemented to fix the paradigm mismatch. In this thesis we develop a framework called PatJ which promotes seamless exploitation of Prolog programming in Java. A sophisticated usage of generics/wildcards allows to define a precise mapping between Object-Oriented and declarative features. PatJ defines a hierarchy of classes where the bidirectional semantics of Prolog terms is modelled directly at the level of the Java generic type-system.

A mixed methods inquiry into the political economy of agriculture and rural areas in Lebanon

The present work, then, is concerned with the forgotten elements of the Lebanese economy, agriculture and rural development. It investigates the main problematic which arose from these forgotten components, in particular the structure of the agricultural sector, production technology, income distribution, poverty, food security, territorial development and local livelihood strategies. It will do so using quantitative Computable General Equilibrium (CGE) modeling and a qualitative phenomenological case study analysis, both embedded in a critical review of the historical development of the political economy of Lebanon, and a structural analysis of its economy. The research shows that under-development in Lebanese rural areas is not due to lack of resources, but rather is the consequence of political choices. It further suggests that agriculture – in both its mainstream conventional and its innovative locally initiated forms of production – still represents important potential for inducing economic growth and development. In order to do so, Lebanon has to take full advantage of its human and territorial capital, by developing a rural development strategy based on two parallel sets of actions: one directed toward the support of local rural development initiatives, and the other directed toward intensive form of production. In addition to its economic returns, such a strategy would promote social and political stability.

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.

The Simon effect and its time courses: an investigation

The objective of the current thesis is to investigate the temporal dynamics (i.e., time courses) of the Simon effect, both from a theoretical and experimental point of view, for a better understanding of whether a) one or more process are responsible for the Simon effect and b) how this/these mechanism/s differently influence performance. In the first theoretical (i.e., “Theoretical Overview”) part, I examined in detail the process and justification for analyzing the temporal dynamics of the Simon effect and the assumptions that underlie interpretation of the results which have been obtained in the existing literature so far. In the second part (“Experimental Investigations”), though, I experimentally investigated several issues which the existing literature left unsolved, in order to get further evidence in favor or in contrast with the mainstream models which are currently used to account for the different Simon effect time courses. Some points about the experiments are worth mentioning: First, all the experiments were conducted in the laboratory, facing participants with stimuli presented on a PC screen and then recording their responses. Both stimuli presentation and response collection was controlled by the E-Prime software. The dependent variables of interest were always behavioral measures of performance, such as velocity and accuracy. Second, the most part of my experiments had been conducted at the Communication Sciences Department (University of Bologna), under Prof. Nicoletti’s supervision. The remaining part, though, had been conducted at the Psychological Sciences Department of Purdue University (West Lafayette, Indiana, USA), where I collaborated for one year as a visiting student with Prof. Proctor and his team. Third, my experimental pool was entirely composed by healthy and young students, since the cognitive functioning of elderly people was not the target of my research.

Engineering Agent-Oriented Technologies and Programming Languages for Computer Programming and Software Development

Mainstream hardware is becoming parallel, heterogeneous, and distributed on every desk, every home and in every pocket. As a consequence, in the last years software is having an epochal turn toward concurrency, distribution, interaction which is pushed by the evolution of hardware architectures and the growing of network availability. This calls for introducing further abstraction layers on top of those provided by classical mainstream programming paradigms, to tackle more effectively the new complexities that developers have to face in everyday programming. A convergence it is recognizable in the mainstream toward the adoption of the actor paradigm as a mean to unite object-oriented programming and concurrency. Nevertheless, we argue that the actor paradigm can only be considered a good starting point to provide a more comprehensive response to such a fundamental and radical change in software development. Accordingly, the main objective of this thesis is to propose Agent-Oriented Programming (AOP) as a high-level general purpose programming paradigm, natural evolution of actors and objects, introducing a further level of human-inspired concepts for programming software systems, meant to simplify the design and programming of concurrent, distributed, reactive/interactive programs. To this end, in the dissertation first we construct the required background by studying the state-of-the-art of both actor-oriented and agent-oriented programming, and then we focus on the engineering of integrated programming technologies for developing agent-based systems in their classical application domains: artificial intelligence and distributed artificial intelligence. Then, we shift the perspective moving from the development of intelligent software systems, toward general purpose software development. Using the expertise maturated during the phase of background construction, we introduce a general-purpose programming language named simpAL, which founds its roots on general principles and practices of software development, and at the same time provides an agent-oriented level of abstraction for the engineering of general purpose software systems.

Vidding Grrls. Pratiche di remix audiovisivo nella cultura digitale contemporanea

La pratica del remix è al giorno d’oggi sempre più diffusa e un numero sempre più vasto di persone ha ora le competenze e gli strumenti tecnologici adeguati per eseguire operazioni un tempo riservate a nicchie ristrette. Tuttavia, nella sua forma audiovisiva, il remix ha ottenuto scarsa attenzione a livello accademico. Questo lavoro esplora la pratica del remix intesa al contempo come declinazione contemporanea di una pratica di lungo corso all’interno della storia della produzione audiovisiva – ovvero il riuso di immagini – sia come forma caratteristica della contemporaneità mediale, atto di appropriazione grassroots dei contenuti mainstream da parte degli utenti. La tesi si articola in due sezioni. Nella prima, l’analisi di tipo teorico e storico-critico è suddivisa in due macro-aree di intervento: da una parte il remix inteso come pratica, atto di appropriazione, gesto di riciclo, decontestualizzazione e risemantizzazione delle immagini mediali che ha attraversato la storia dei media audiovisivi [primo capitolo]. Dall’altra, la remix culture, ovvero il contesto culturale e sociale che informa l’ambiente mediale entro il quale la pratica del remix ha conosciuto, nell’ultimo decennio, la diffusione capillare che lo caratterizza oggi [secondo capitolo]. La seconda, che corrisponde al terzo capitolo, fornisce una dettagliata panoramica su un caso di studio, la pratica del fan vidding. Forma di remix praticata quasi esclusivamente da donne, il vidding consiste nel creare fan video a partire da un montaggio d’immagini tratte da film o serie televisive che utilizza come accompagnamento musicale una canzone. Le vidders, usando specifiche tecniche di montaggio, realizzano delle letture critiche dei prodotti mediali di cui si appropriano, per commentare, criticare o celebrare gli oggetti di loro interesse. Attraverso il vidding il presente lavoro indaga le tattiche di rielaborazione e riscrittura dell’immaginario mediale attraverso il riuso di immagini, con particolare attenzione al remix inteso come pratica di genere.

Scienza della sostenibilita' e regolazione: Il caso studio della politica europea in materia di risparmio energetico

Entro l’approccio concettuale e metodologico transdisciplinare della Scienza della Sostenibilità, la presente tesi elabora un background teorico per concettualizzare una definizione di sostenibilità sulla cui base proporre un modello di sviluppo alternativo a quello dominante, declinato in termini di proposte concrete entro il caso-studio di regolazione europea in materia di risparmio energetico. La ricerca, attraverso un’analisi transdisciplinare, identifica una crisi strutturale del modello di sviluppo dominante basato sulla crescita economica quale (unico) indicatore di benessere e una crisi valoriale. L’attenzione si concentra quindi sull’individuazione di un paradigma idoneo a rispondere alle criticità emerse dall’analisi. A tal fine vengono esaminati i concetti di sviluppo sostenibile e di sostenibilità, arrivando a proporre un nuovo paradigma (la “sostenibilità ecosistemica”) che dia conto dell’impossibilità di una crescita infinita su un sistema caratterizzato da risorse limitate. Vengono poi presentate delle proposte per un modello di sviluppo sostenibile alternativo a quello dominante. Siffatta elaborazione teorica viene declinata in termini concreti mediante l’elaborazione di un caso-studio. A tal fine, viene innanzitutto analizzata la funzione della regolazione come strumento per garantire l’applicazione pratica del modello teorico. L’attenzione è concentrata sul caso-studio rappresentato dalla politica e regolazione dell’Unione Europea in materia di risparmio ed efficienza energetica. Dall’analisi emerge una progressiva commistione tra i due concetti di risparmio energetico ed efficienza energetica, per la quale vengono avanzate delle motivazioni e individuati dei rischi in termini di effetti rebound. Per rispondere alle incongruenze tra obiettivo proclamato dall’Unione Europea di riduzione dei consumi energetici e politica effettivamente perseguita, viene proposta una forma di “regolazione per la sostenibilità” in ambito abitativo residenziale che, promuovendo la condivisione dei servizi energetici, recuperi il significato proprio di risparmio energetico come riduzione del consumo mediante cambiamenti di comportamento, arricchendolo di una nuova connotazione come “bene relazionale” per la promozione del benessere relazionale ed individuale.

Normare la vita. Biocontrollo e nuove tecnologie

Questa ricerca, suddivisa in due parti, si concentra sulle problematiche connesse alla normazione della vita e dei corpi delle donne al tempo delle biotecnologie. La Parte I è una genealogia filosofico-politica che ripercorre le tappe analitico-concettuali del dibattito intorno a biopolitica e tecnoscienza, a partire dai contributi teorici di poststrutturalismo e femminismo neomaterialista, e risponde alle domande: Cosa sono diventati i corpi nell’attuale società bio-info-modificata? Qual'è il ruolo delle scienze nelle metamorfosi che interessano soggettività e rapporti di potere? La Parte II è una cartografia dei modi in cui le biotecnologie, riguardanti i corpi delle donne, si sono sviluppate e diffuse. Essa indaga in modo transdisciplinare come in Italia, e più in generale in Europa, sono state normate le tecniche di interruzione volontaria di gravidanza e fecondazione in vitro. Ampio spazio è dedicato ai modi in cui gli attori della bioetica, istituzionale e non, i medici, laici e cattolici, e le case farmaceutiche hanno affrontato questi temi e quello della contraccezione ormonale maschile. Medicina riproduttiva e rigenerativa sono tematizzate sempre in relazione al quadro normativo, per mostrare in che modo esso influenzi l’accesso ai diritti alla salute e all’autodeterminazione delle donne. Il quadro normativo è analizzato, a sua volta, alla luce dei fatti storici più rilevanti e delle culture più diffuse. L’obiettivo della ricerca è duplice: da un lato essa ha il fine di mostrare il modo in cui i corpi delle donne, e la relativa potenza generatrice, siano diventati uno snodo fondamentale nell’articolazione del biocontrollo e nell'apertura dei nuovi mercati legati a medicina riproduttiva e rigenerativa; dall’altro si propone di argomentare come un biodiritto flessibile, a contenuto storico variabile, condiviso e partecipato, sia un’ipotesi praticabile e virtuosa, utile all'eliminazione del gender gap ancora esistente in materia di diritti riproduttivi e sessuali.