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

Abstract

Abstract

Abstract
Multimodal models, namely vision-language models, present unique possibilities through the seamless integration of different information mediums for data generation. These models mostly act as a black-box, making them lack transparency and explicability. Reliable results require accountable and trustworthy Artificial Intelligence (AI), namely when in use for critical tasks, such as the automatic generation of medical imaging reports for healthcare diagnosis. By exploring stress-testing techniques, multimodal generative models can become more transparent by disclosing their shortcomings, further supporting their responsible usage in the medical field. Copyright © 2025, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

Abstract
With technological advancements, much data is being captured by sensors, smartphones, wearable devices, and so forth. These vast datasets are stored in data centres and utilized to forge data-driven models for the condition monitoring of infrastructures and systems through future data mining tasks. However, these datasets often surpass the processing capabilities of traditional information systems and methodologies due to their significant size. Additionally, not all samples within these datasets contribute valuable information during the model training phase, leading to inefficiencies. The processing and training of Machine Learning algorithms become time-consuming, and storing all the data demands excessive space, contributing to the Big Data challenge. In this paper, we propose two novel techniques to reduce large time-series datasets into more compact versions without undermining the predictive performance of the resulting models. These methods also aim to decrease the time required for training the models and the storage space needed for the condensed datasets. We evaluated our techniques on five public datasets, employing three Machine Learning algorithms: Holt-Winters, SARIMA, and LSTM. The outcomes indicate that for most of the datasets examined, our techniques maintain, and in several instances enhance, the forecasting accuracy of the models. Moreover, we significantly reduced the time required to train the Machine Learning algorithms employed.