Abstract
Conflict-free Replicated Data Types (CRDTs) are a very popular class of distributed data structures that strike a compromise between strong and eventual consistency. Ensuring the protection of data stored within a CRDT, however, cannot be done trivially using standard encryption techniques, as secure CRDT protocols would require replica-side computation. This paper proposes an approach to lift general-purpose implementations of CRDTs to secure variants using secure multiparty computation (MPC). Each replica within the system is realized by a group of MPC parties that compute its functionality. Our results include: i) an extension of current formal models used for reasoning over the security of CRDT solutions to the MPC setting; ii) a MPC language and type system to enable the construction of secure versions of CRDTs and; iii) a proof of security that relates the security of CRDT constructions designed under said semantics to the underlying MPC library. We provide an open-source system implementation with an extensive evaluation, which compares different designs with their baseline throughput and latency.

Abstract
Approximate agreement has long been relegated to the sidelines compared to exact consensus, with its most notable application being clock synchronisation. Other proposed applications stemming from control theory target multi-agent consensus, namely for sensor stabilisation, coordination in robotics, and trust estimation. Several proposals for approximate agreement follow the Mean Subsequence Reduce approach, simply applying different functions at each phase. However, taking clock synchronisation as an example, applications do not fit neatly into the MSR model: Instead they require adapting the algorithms' internals. Our contribution is two-fold. First, we identify additional configuration points, establishing a more general template of MSR approximate agreement algorithms. We then show how this allows us to implement not only generic algorithms but also those tailored for specific purposes (clock synchronisation). Second, we propose a toolkit for making approximate agreement practical, providing classical implementations as well as allow these to be configured for specific purposes. We validate the implementation with classical algorithms and clock synchronisation.

Abstract
The development of more flexible and robust models for reasoning about systems in environments with potentially conflicting information is becoming more and more relevant in different contexts. In this direction, we recently introduced paraconsistent transition systems, i.e. transition systems whose transitions are tagged with a pair of weights, one standing for the degree of evidence that the transition exists, another weighting its potential non existence. Moreover, these structures were endowed with a modal logic [3] that was further formalised as an institution in [5]. This paper goes a step further, proposing an approach for the structured specification of paraconsistent transition processes, i.e. paraconsistent transition systems with initial states. The proposed approach is developed along the lines of [12], which introduced a complete methodology for (standard) reactive systems development building on the Sannella and Tarlecki stepwise implementation process. For this, we enrich the logic with dynamic modalities and hybrid features, and provide a pallet of constructors and abstractors to support the development process of paraconsistent processes along the entire design cycle.

Abstract
Immersive video applications impose unpractical bandwidth requirements for best-effort networks. With Multi-View(MV) streaming, these can be minimized by resorting to view prediction techniques. SmoothMV is a multi-view system that uses a non-intrusive head tracking mechanism to detect the viewer's interest and select appropriate views. By coupling Neural Networks (NNs) to anticipate the viewer's interest, a reduction of view-switching latency is likely to be obtained. The objective of this paper is twofold: 1) Present a solution for acquisition of gaze data from users when viewing MV content; 2) Describe a dataset, collected with a large-scale testbed, capable of being used to train NNs to predict the user's viewing interest. Tracking data from head movements was obtained from 45 participants using an Intel Realsense F200 camera, with 7 video playlists, each being viewed a minimum of 17 times. This dataset is publicly available to the research community and constitutes an important contribution to reducing the current scarcity of such data. Tools to obtain saliency/heat maps and generate complementary plots are also provided as an open-source software package.

Abstract
There are several educational software (ES) used in the classroom environment for the teaching and learning of geometric contents that are part of the Portuguese basic education mathematics program. There are studies that show that the use of this type of artifact has a fundamental role in the behavior of students, raising, among other aspects, a greater motivation for learning mathematics. The aim of this work is to explore and describe implications for the behavior and learning of students in the 7th grade of Portuguese basic education, in face of a pedagogical practice that involves carrying out tasks using ES Plickers, in the theme similarities of the domain geometry and measurement, throughout intervention carried out. The adopted methodology presents characteristics of a quasi-experimental study. The participants were 61 students from three classes of a school in the north of Portugal, followed during eight consecutive classes. A set of tasks using Plickers, tests and a questionnaire survey were used as instruments for data collection. The results point to positive increments, at a behavioral level, as well as in the evolution of learning, in view of the use of this methodology in the classroom.

Abstract
As gamification spreads to new areas, new applications are being developed and the interest in evaluating gamified systems continues to grow. To date, however, no one has comprehensively approached this topic: multiple evaluation dimensions and measures have been proposed and applied without any effort to organize them into a full gamut of tools for the multi-dimensional evaluation of gamified systems. This paper addresses this gap by proposing GATUGU, a set of six perspectives of evaluation of gamified systems: General effects of gamification, Area-specific effects of gamification, Technical quality of gamified systems, Use of gamified systems, Gamefulness of gamified systems, and User experience of gamified systems. For each perspective, GATUGU indicates the relevant dimensions of evaluation, and, for each dimension, one measure is suggested. GATUGU does not introduce any new measurement tools but merely recommends one of the available tools for each dimension, considering their popularity and ease of use. GATUGU can guide researchers in selecting gamification system evaluation perspectives and dimensions and in finding adequate measurement tools. Thanks to conforming to GATUGU, the published gamification system evaluation results will become easier to compare and to perform various kinds of meta-analyses on them.