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.

Performing inclusion and exclusion in the peer group. Children's social organization and peer socializing practices in the classroom

This PhD thesis investigates children’s peer practices in two primary schools in Italy, focusing on the ordinary and the Italian L2 classroom. The study is informed by the paradigm of language socialization and considers peer interactions as a ‘double opportunity space’, allowing both children’s co-construction of their social organization and children’s sociolinguistic development. These two foci of attention are explored on the basis of children’s social interaction and of the verbal, embodied, and material resources that children agentively deploy during their mundane activities in the peer group. The study is based on a video ethnography that lasted nine months. Approximately 30 hours of classroom interactions were video-recorded, transcribed, and analyzed with an approach that combines the micro-analytic instruments of Conversation Analysis and the use of ethnographic information. Three main social phenomena were selected for analysis: (a) children’s enactment of the role of the teacher, (b) children’s reproduction of must-formatted rules, and (c) children’s argumentative strategies during peer conflict. The analysis highlights the centrality of the institutional frame for children’s peer interactions in the classroom. Moreover, the study illustrates that children socialize their classmates to the linguistic, social, and moral expectations of the context in and through various practices. Notably, these practices are also germane to the local negotiation of children’s social organization and hierarchy. Therefore, the thesis underlines that children’s peer interactions are both a resource for children’s sociolinguistic development and a potentially problematic locus where social exclusion is constructed and brought to bear. These insights are relevant for teachers’ professional practice. Children’s peer interactions are a resource that can be integrated in everyday didactics. Nevertheless, the role of the teacher in supervising and steering children’s peer practices appears crucial: an acritical view of children’s autonomous work, often implied in teaching methods such as peer tutoring, needs to be problematized.

Oceanic Near-inertial internal waves generation, propagation and interaction with mesoscale dynamics

Oceans play a key role in the climate system, being the largest heat sinks on Earth. Part of the energy balance of ocean circulation is driven by the Near-inertial internal waves (NIWs). Strong NIWs are observed during a multi-platform, multi-disciplinary and multi-scale campaign led by the NATO-STO CMRE in autumn 2017 in the Ligurian Sea (northwestern Mediterranean Sea). The objectives of this work are as follows: characterise the studied area at different scales; study the NIWs generation and their propagation; estimate the NIWs properties; study the interaction between NIWs and mesoscale structures. This work provides, to the author’s knowledge, the first characterization of NIWs in the Mediterranean Sea. The near-surface NIWs observed at the fixed moorings are locally generated by wind bursts while the deeper waves originate in other regions and arrive at the moorings several days later. Most of the observed NIWs energy propagates downward with a mean vertical group velocity of (2.2±0.3) ⋅10-4 m s-1. On average, the NIWs have an amplitude of 0.13 m s-1 and mean horizontal and vertical wavelengths of 43±25 km and 125±35 m, while shorter wavelengths are observed at the near-coastal mooring, 36±2 km and 33±2 m, respectively. Most of the observed NIWs are blue shifted and reach a value 9% higher than the local inertial frequency. Only two observed NIWs are characterised by a redshift (up to 3% lower than the local inertial frequency). In support of the in situ observations, a high resolution numerical model is implemented using NEMO (Madec et al., 2019). Results show that anticyclones (cyclones) shift the frequency of NIWs to lower (higher) frequencies with respect to the local inertial frequency. Anticyclones facilitate the downward propagation of NIW energy, while cyclones dampen it. Absence of NIWs energy within an anticyclone is also investigated.