Abstract
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.

Abstract
The use of digital games as support tools for education has proven to be effective. To explore their potential, it is crucial to design them carefully. This chapter considers the design of games for education, where players cultivate their knowledge and practice their skills by multiplying numerous hindrances during gaming. Educational elements are integrated into the gameplay, which players acquire while playing. The game's effectiveness depends on the players' ability to form a cheerful and encouraging environment to continue playing while increasing their interest in gameplay and improving academic performance. Following a design-first development approach, an innovative proposal for this design is presented, adding a new dimension to the game's tetrad: learning dynamics. Benefiting from years of professional practice, this game pentad design framework fulfills the learning and user experience requirements while overcoming the design limitations of more conventional approaches not based on an educational purpose.

Abstract
Virtual reality (VR) potential to isolate users from the real world while producing a rich virtual environment where users act similarly to how they would, in reality, is still being investigated in several fields. In this work, we investigated the effects of product contextualisation and gender under an immersive VR application where users can explore in-depth a commercial product with a hands-on experience. An experimental between-subjects study was performed with 38 participants between 18 and 28 years. The product tested consisted of a double-door refrigerator equipped with a touchscreen. Two independent variables were studied: Context (the refrigerator was filled with food products and placed in a kitchen), Neutral Context (empty refrigerator displayed in an empty white room), and Gender (Female and Male). As for the dependent variables, we considered how clarified users felt about the product functionalities, its size, the extent users remember details and characteristics of the refrigerator, and the user's subjective workload. The evidence shows that contextualisation and gender have no impact on any dependent variables. Therefore, we concluded that presenting a product in its context does not benefit significantly benefit it. Thus, opting for a neutral context would be preferable to save computational costs and human resources necessary to build and run the higher complexity environments required to contextualise the product.

Abstract
Container orchestration tools supporting infrastructure-as-code allow new forms of collaboration between developers and operatives. Still, their text-based nature permits naive mistakes and is more difficult to read as complexity increases. We can find few examples of low-code approaches for defining the orchestration of containers, and there seems to be a lack of empirical studies showing the benefits and limitations of such approaches. We hypothesize that a complete visual notation for Docker-based orchestrations could reduce the effort, the error rate, and the development time. Therefore, we developed a tool featuring such a visual notation for Docker Compose configurations, and we empirically evaluated it in a controlled experiment with novice developers. The results show a significant reduction in development time and error-proneness when defining Docker Compose files, supporting our hypothesis. The participants also thought the prototype easier to use and useful, and wanted to use it in the future.

Abstract
Many techniques have contributed to the advancement of automated program repair, such as: generate and validate approaches, constraint-based solvers and even neural machine translation. Simultaneously, artificial intelligence has allowed the creation of general-purpose pre-trained models that support several downstream tasks. In this paper, we describe a technique that takes advantage of a generative model - CodeGPT - to automatically repair buggy programs by making use of its code completion capabilities. We also elaborate on where to perform code completion in a buggy line and how we circumvent the open-ended nature of code generation to appropriately fit the new code in the original program. Furthermore, we validate our approach on the ManySStuBs4j dataset containing real-world open-source projects and show that our tool is able to fix 1739 programs out of 6415 - a 27% repair rate. The repaired programs range from single-line changes to multiple line modifications. In fact, our technique is able to fix programs which were missing relatively complex expressions prior to being analyzed. In the end, we present case studies that showcase different scenarios our technique was able to handle.

Abstract
The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, and the declarative semantics, which sees logic programs as formulas and its semantics as models. Here, we define a new operational semantics called TSLD-resolution, which stands for Typed SLD-resolution, where we include a value wrong, that corresponds to the detection of a type error at run-time. For this we define a new typed unification algorithm. Finally we prove the correctness of TSLD-resolution with respect to a typed declarative semantics.