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.

Evidenze micropaleontologiche e sedimentologiche di cicli deposizionali e climatici circa millenari nei Depositi Tardoquaternari della Piana dell'Arno e del Delta del Po

A multidisciplinary study was carried out on the Late Quaternary-Holocene subsurface deposits of two Mediterranean coastal areas: Arno coastal plain (Northern Tyrrhenian Sea) and Modern Po Delta (Northern Adriatic Sea). Detailed facies analyses, including sedimentological and micropalaeontological (benthic foraminifers and ostracods) investigations, were performed on nine continuously-cored boreholes of variable depth (ca. from 30 meters to100 meters). Six cores were located in the Arno coastal plain and three cores in the Modern Po Delta. To provide an accurate chronological framework, twenty-four organic-rich samples were collected along the fossil successions for radiocarbon dating (AMS 14C). In order to reconstruct the depositional and palaeoenvironmental evolution of the study areas, core data were combined with selected well logs, provided by local companies, along several stratigraphic sections. These sections revealed the presence of a transgressive-regressive (T-R) sequence, composing of continental, coastal and shallow-marine deposits dated to the Late Pleistocene-Holocene period, beneath the Arno coastal plain and the Modern Po Delta. Above the alluvial deposits attributed to the last glacial period, the post-glacial transgressive succession (TST) consists of back-barrier, transgressive barrier and inner shelf deposits. Peak of transgression (MFS) took place around the Late-Middle Holocene transition and was identified by subtle micropalaeontological indicators within undifferentiated fine-grained deposits. Upward a thick prograding succession (HST) records the turnaround to regressive conditions that led to a rapid delta progradation in both study areas. Particularly, the outbuilding of modern-age Po Delta coincides with mud-belt formation during the late HST (ca. 600 cal yr BP), as evidenced by a fossil microfauna similar to the foraminiferal assemblage observed in the present Northern Adriatic mud-belt. A complex interaction between allocyclic and autocyclic factors controlled facies evolution during the highstand period. The presence of local parameters and the absence of a predominant factor prevent from discerning or quantifying consequences of the complex relationships between climate and deltaic evolution. On the contrary transgressive sedimentation seems to be mainly controlled by two allocyclic key factors, sea-level rise and climate variability, that minimized the effects of local parameters on coastal palaeoenvironments. TST depositional architecture recorded in both study areas reflects a well-known millennial-scale variability of sea-level rising trend and climate during the Late glacial-Holocene period. Repeated phases of backswamp development and infilling by crevasse processes (parasequences) were recorded in the subsurface of Modern Po Delta during the early stages of transgression (ca. 11,000-9,500 cal yr BP). In the Arno coastal plain the presence of a deep-incised valley system, probably formed at OSI 3/2 transition, led to the development of a thick (ca. 35-40 m) transgressive succession composed of coastal plain, bay-head delta and estuarine deposits dated to the Last glacial-Early Holocene period. Within the transgressive valley fill sequence, high-resolution facies analyses allowed the identification and lateral tracing of three parasequences of millennial duration. The parasequences, ca. 8-12 meters thick, are bounded by flooding surfaces and show a typical internal shallowing-upward trend evidenced by subtle micropalaeontological investigations. The vertical stacking pattern of parasequences shows a close affinity with the step-like sea-level rising trend occurred between 14,000-8,000 cal years BP. Episodes of rapid sea-level rise and subsequent stillstand phases were paralleled by changes in climatic conditions, as suggested by pollen analyses performed on a core drilled in the proximal section of the Arno palaeovalley (pollen analyses performed by Dr. Marianna Ricci Lucchi). Rapid shifts to warmer climate conditions accompanied episodes of rapid sea-level rise, in contrast stillstand phases occurred during temporary colder climate conditions. For the first time the palaeoclimatic signature of high frequency depositional cycles is clearly documented. Moreover, two of the three "regressive" pulsations, recorded at the top of parasequences by episodes of partial estuary infilling in the proximal and central portions of Arno palaeovalley, may be correlated with the most important cold events of the post-glacial period: Younger Dryas and 8,200 cal yr BP event. The stratigraphic and palaeoclimatic data of Arno coastal plain and Po Delta were compared with those reported for the most important deltaic and coastal systems in the worldwide literature. The depositional architecture of transgressive successions reflects the strong influence of millennial-scale eustatic and climatic variability on worldwide coastal sedimentation during the Late glacial-Holocene period (ca. 14,000-7,000 cal yr BP). The most complete and accurate record of high-frequency eustatic and climatic events are usually found within the transgressive succession of very high accommodation settings, such as incised-valley systems where exceptionally thick packages of Late glacial-Early Holocene deposits are preserved.

Percorsi di gender performance: fotografia tra arte e moda dagli anni Novanta ad oggi

My project explores and compares different forms of gender performance in contemporary art and visual culture according to a perspective centered on photography. Thanks to its attesting power this medium can work as a ready-made. In fact during the 20th century it played a key role in the cultural emancipation of the body which (using a Michel Foucault’s expression) has now become «the zero point of the world». Through performance the body proves to be a living material of expression and communication while photography ensures the recording of any ephemeral event that happens in time and space. My questioning approach considers the gender constructed imagery from the 1990s to the present in order to investigate how photography’s strong aura of realism promotes and allows fantasies of transformation. The contemporary fascination with gender (especially for art and fashion) represents a crucial issue in the global context of postmodernity and is manifested in a variety of visual media, from photography to video and film. Moreover the internet along with its digital transmission of images has deeply affected our world (from culture to everyday life) leading to a postmodern preference for performativity over the more traditional and linear forms of narrativity. As a consequence individual borders get redefined by the skin itself which (dissected through instant vision) turns into a ductile material of mutation and hybridation in the service of identity. My critical assumptions are taken from the most relevant changes occurred in philosophy during the last two decades as a result of the contributions by Jacques Lacan, Michel Foucault, Jacques Derrida, Gilles Deleuze who developed a cross-disciplinary and comparative approach to interpret the crisis of modernity. They have profoundly influenced feminist studies so that the category of gender has been reassessed in contrast with sex (as a biological connotation) and in relation to history, culture, society. The ideal starting point of my research is the year 1990. I chose it as the approximate historical moment when the intersection of race, class and gender were placed at the forefront of international artistic production concerned with identity, diversity and globalization. Such issues had been explored throughout the 1970s but it was only from the mid-1980s onward that they began to be articulated more consistently. Published in 1990, the book "Gender trouble: feminism and the subversion of identity" by Judith Butler marked an important breakthrough by linking gender to performance as well as investigating the intricate connections between theory and practice, embodiment and representation. It inspired subsequent research in a variety of disciplines, art history included. In the same year Teresa de Lauretis launched the definition of queer theory to challenge the academic perspective in gay and lesbian studies. In the meantime the rise of Third Wave Feminism in the US introduced a racially and sexually inclusive vision over the global situation in order to reflect on subjectivity, new technologies and popular culture in connection with gender representation. These conceptual tools have enabled prolific readings of contemporary cultural production whether fine arts or mass media. After discussing the appropriate framework of my project and taking into account the postmodern globalization of the visual, I have turned to photography to map gender representation both in art and in fashion. Therefore I have been creating an archive of images around specific topics. I decided to include fashion photography because in the 1990s this genre moved away from the paradigm of an idealized and classical beauty toward a new vernacular allied with lifestyles, art practices, pop and youth culture; as one might expect the dominant narrative modes in fashion photography are now mainly influenced by cinema and snapshot. These strategies originate story lines and interrupted narratives using models’ performance to convey a particular imagery where identity issues emerge as an essential part of fashion spectacle. Focusing on the intersections of gender identities with socially and culturally produced identities, my approach intends to underline how the fashion world has turned to current trends in art photography and in some case turned to the artists themselves. The growing fluidity of the categories that distinguish art from fashion photography represents a particularly fruitful moment of visual exchange. Varying over time the dialogue between these two fields has always been vital; nowadays it can be studied as a result of this close relationship between contemporary art world and consumer culture. Due to the saturation of postmodern imagery the feedback between art and fashion has become much more immediate and then increasingly significant for anyone who wants to investigate the construction of gender identity through performance. In addition to that a lot of magazines founded in the 1990s bridged the worlds of art and fashion because some of their designers and even editors were art-school graduates encouraging innovation. The inclusion of art within such magazines aimed at validating them as a form of art in themselves supporting a dynamic intersection for music, fashion, design and youth culture: an intersection that also contributed to create and spread different gender stereotypes. This general interest in fashion produced many exhibitions of and about fashion itself at major international venues such as the Victoria and Albert Museum in London, the Metropolitan Museum of Art and the Solomon R. Guggenheim Museum in New York. Since then this celebrated success of fashion has been regarded as a typical element of postmodern culture. Owing to that I have also based my analysis on some important exhibitions dealing with gender performance like "Féminin-Masculin" at the Centre Pompidou of Paris (1995), "Rrose is a Rrose is a Rrose. Gender performance in photography" at the Solomon R. Guggenheim Museum of New York (1997), "Global Feminisms" at the Brooklyn Museum (2007), "Female Trouble" at the Pinakothek der Moderne in München together with the workshops dedicated to "Performance: gender and identity" in June 2005 at the Tate Modern of London. Since 2003 in Italy we have had Gender Bender - an international festival held annually in Bologna - to explore the gender imagery stemming from contemporary culture. In few days this festival offers a series of events ranging from visual arts, performance, cinema, literature to conferences and music. Being aware that any method of research is neither race nor gender neutral I have traced these critical paths to question gender identity in a multicultural perspective taking account of the political implications too. In fact, if visibility may be equated with exposure, we can also read these images as points of intersection of visibility with social power. Since gender assignations rely so heavily on the visual, the postmodern dismantling of gender certainty through performance has wide-ranging effects that need to be analyzed. In some sense this practice can even contest the dominance of visual within postmodernism. My visual map in contemporary art and fashion photography includes artists like Nan Goldin, Cindy Sherman, Hellen van Meene, Rineke Dijkstra, Ed Templeton, Ryan McGinley, Anne Daems, Miwa Yanagi, Tracey Moffat, Catherine Opie, Tomoko Sawada, Vanessa Beecroft, Yasumasa Morimura, Collier Schorr among others.

Social learning and action understanding in human observers: contributions of sensori-motor constraints and prior information

The aim of this thesis was to investigate the respective contribution of prior information and sensorimotor constraints to action understanding, and to estimate their consequences on the evolution of human social learning. Even though a huge amount of literature is dedicated to the study of action understanding and its role in social learning, these issues are still largely debated. Here, I critically describe two main perspectives. The first perspective interprets faithful social learning as an outcome of a fine-grained representation of others’ actions and intentions that requires sophisticated socio-cognitive skills. In contrast, the second perspective highlights the role of simpler decision heuristics, the recruitment of which is determined by individual and ecological constraints. The present thesis aims to show, through four experimental works, that these two contributions are not mutually exclusive. A first study investigates the role of the inferior frontal cortex (IFC), the anterior intraparietal area (AIP) and the primary somatosensory cortex (S1) in the recognition of other people’s actions, using a transcranial magnetic stimulation adaptation paradigm (TMSA). The second work studies whether, and how, higher-order and lower-order prior information (acquired from the probabilistic sampling of past events vs. derived from an estimation of biomechanical constraints of observed actions) interacts during the prediction of other people’s intentions. Using a single-pulse TMS procedure, the third study investigates whether the interaction between these two classes of priors modulates the motor system activity. The fourth study tests the extent to which behavioral and ecological constraints influence the emergence of faithful social learning strategies at a population level. The collected data contribute to elucidate how higher-order and lower-order prior expectations interact during action prediction, and clarify the neural mechanisms underlying such interaction. Finally, these works provide/open promising perspectives for a better understanding of social learning, with possible extensions to animal models.

Automatic Deployment of Applications in the Cloud

In distributed systems like clouds or service oriented frameworks, applications are typically assembled by deploying and connecting a large number of heterogeneous software components, spanning from fine-grained packages to coarse-grained complex services. The complexity of such systems requires a rich set of techniques and tools to support the automation of their deployment process. By relying on a formal model of components, a technique is devised for computing the sequence of actions allowing the deployment of a desired configuration. An efficient algorithm, working in polynomial time, is described and proven to be sound and complete. Finally, a prototype tool implementing the proposed algorithm has been developed. Experimental results support the adoption of this novel approach in real life scenarios.

The language of others mirrored in thy face: The role of political affiliation in automatic facial effects of language

People tend to automatically mimic facial expressions of others. If clear evidence exists on the effect of non-verbal behavior (emotion faces) on automatic facial mimicry, little is known about the role of verbal behavior (emotion language) in triggering such effects. Whereas it is well-established that political affiliation modulates facial mimicry, no evidence exists on whether this modulation passes also through verbal means. This research addressed the role of verbal behavior in triggering automatic facial effects depending on whether verbal stimuli are attributed to leaders of different political parties. Study 1 investigated the role of interpersonal verbs, referring to positive and negative emotion expressions and encoding them at different levels of abstraction, in triggering corresponding facial muscle activation in a reader. Study 2 examined the role of verbs expressing positive and negative emotional behaviors of political leaders in modulating automatic facial effects depending on the matched or mismatched political affiliation of participants and politicians of left-and right-wing. Study 3 examined whether verbs expressing happiness displays of ingroup politicians induce a more sincere smile (Duchenne) pattern among readers of same political affiliation relative to happiness expressions of outgroup politicians. Results showed that verbs encoding facial actions at different levels of abstraction elicited differential facial muscle activity (Study 1). Furthermore, political affiliation significantly modulated facial activation triggered by emotion verbs as participants showed more congruent and enhanced facial activity towards ingroup politicians’ smiles and frowns compared to those of outgroup politicians (Study 2). Participants facially responded with a more sincere smile pattern towards verbs expressing smiles of ingroup compared to outgroup politicians (Study 3). Altogether, results showed that the role of political affiliation in modulating automatic facial effects passes also through verbal channels and is revealed at a fine-grained level by inducing quantitative and qualitative differences in automatic facial reactions of readers.

Mass Loss in Population II Red Giants: an IRAC@Spitzer Survey of Galactic Globular Clusters

With the goal of studying ML along the RGB, mid-IR observations of a carefully selected sample of 17 Galactic globular clusters (GGCs) with different metallicity and horizontal branch (HB) morphology have been secured with IRAC on board Spitzer: a global sample counting about 8000 giant has been obtained. Suitable complementary photometry in the optical and near-IR has been also secured in order to properly characterize the stellar counterparts to the Spitzer sources and their photospheric parameters. Stars with color (i.e. dust) excess have been identified, their likely circumstellar emission quantified and modelled, and empirical estimates of mass loss rates and timescales obtained. We find that mass loss rates increases with increasing stellar luminosity and decreasing metallicity. For a given luminosity, we find that ML rates are systematically higher than the prediction by extrapolating the Reimers law. CMDs constructed from ground based near-IR and IRAC bands show that at a given luminosity some stars have dusty envelopes and others do not. From this, we deduce that the mass loss is episodic and is ``on'' for some fraction of the time. The total mass lost on the RGB can be easily computed by multiplying ML rates by the ML timescales and integrating over the evolutionary timescale. The average total mass lost moderately increases with increasing metallicity, and for a given metallicity is systematically higher in clusters with extended blue HB.