Abstract
Artificial Intelligence (AI), in particular Generative Artificial Intelligence (GenAI), is a quickly developing field capable of revolutionizing educational digital escape rooms. Traditionally reliant on static content, these immersive environments have faced limitations in adaptability, replayability, and personalization. However, recent advancements in AI and GenAI enable dynamic puzzle generation, adaptive storytelling, and AI-driven non-player characters (NPCs) with agentic AI, allowing for highly responsive and personalized experiences. This paper reviews the state-of-the-art in integrating AI (with the focus on GenAI) into educational digital escape rooms, integrating interdisciplinary insights from cognitive science, game design, and machine learning, and showing how AI can improve engagement, scalability, and content diversity, but also indicates challenges related to ethical AI use, bias in algorithmic decision-making, and the need for robust evaluation frameworks to assess player satisfaction and learning outcomes. © 2025 Elsevier B.V., All rights reserved.

Abstract
This paper presents an overview of the FGPE (Framework for Gamified Programming Education), a set of three Erasmus+ projects aimed at providing a framework for applying gamification to programming education. The overview will encompass all three phases of the framework development, emphasizing the gamification elements embedded in the design and implementation of the outputs of each phase. These outputs will be presented as a unified narrative, including the gamification framework for programming exercises, a format for defining gamification details for programming exercises and courses, the authoring tool for the gamification layer, a gamification Web service, a tutorial on gamifying programming exercises (guidance material), and a tool that automatically generates gamified programming exercises.

Abstract
This paper presents the guidelines for game experiences integration into Learning Management Systems (LMS) through the IMS LTI (Learning Tools Interoperability) specification. At the same time, it also introduces a dynamic scoring formula, based on a given taxonomy, that goes beyond traditional metrics, allowing for the inclusion of any number of game elements, such as levels, challenges, hints used, and time taken, within the game framework. These elements are assigned weight factors, which can be configured by instructors within the LMS platform, facilitating personalized assessment criteria tailored to specific learning objectives. In order to apply these approach in a real educational scenario, an Escape Room (ER) for math skills testing was used. Using the LTI specification for integration in combination with the dynamic scoring formula provides a comprehensive assessment of student performance, giving a single score which will be vital to enhance the LMS gamified workflow. This research contributes to the field of gamification in education, offering insights into the integration of (serious or regular) games in LMS platforms.

Abstract
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we use a (weak and closed) lambda-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this language not only encodes Plotkin's CBV and CBN lambda-calculus as well as other subsuming frameworks, such as the bang-calculus, but can also be used to interpret the semantics of effectful languages with exceptions. After a thorough study of the untyped language, we introduce a type system based on intersection types, and we show through purely logical methods that the set of terminating terms of the language corresponds exactly to that of well-typed terms. Moreover, by considering non-idempotent intersection types, this characterization turns out to be quantitative, i.e. the size of the type derivation of a term t gives an upper bound for the number of evaluation steps from t to its normal form.

Abstract
We show that recent approaches to quantitative analysis based on non-idempotent typing systems can be extended to programming languages with effects. In particular, we consider two cases: the weak open call-by-name (CBN) and call-by-value (CBV) variants of the $\lambda$ -calculus, equipped with operations to write and read from a global state. In order to capture quantitative information with respect to time and space for both CBN and CBV, we design for each of them a quantitative type system based on a (tight) multi-type system. One key observation of this work is how CBN and CBV influence the composition of state types. That is, each type system is developed by taking into account how each language manages the global state: in CBN, the composition of state types is almost straightforward, since function application does not require evaluation of its argument; in CBV, however, the interaction between functions and arguments makes the composition of state types more subtle since only values can be passed as actual arguments. The main contribution of this paper is the design of type systems capturing quantitative information about effectful CBN and CBV programming languages. Indeed, we develop type systems that are qualitatively and quantitatively sound and complete.

Abstract
In recent years, code-reuse attacks have been used to exploit software vulnerabilities and gain control of numerous software programs and embedded devices. Several measures have been put in place to prevent this type of attack, such as Control-Flow Integrity (CFI) systems, and some of these systems have already been integrated into hardware. Nevertheless, Function-Oriented Programming (FOP) attacks, a form of code-reuse that chains functions to carry out malicious actions, continue to persist. In this work, we present the first analysis of the implications and feasibility of FOP attacks on microcontrollers, focusing on ARM Cortex-M processors that support PACBTI, that is, a hardware feature designed for CFI system implementation. During this process, we identified multiple dispatch gadgets in two common Real-time Operating System (RTOS). Since these gadgets reside within core OS functionalities, they are inherently included in a broad range of embedded operating systems. Furthermore, we also present CortexMFopper - a tool specially built to identify FOP gadgets in embedded devices and to raise awareness of this technique.