Abstract
Interest in artificial intelligence (AI)-driven crowd work has increased during the last few years as a line of inquiry that expands upon prior research on microtasking to represent a means of scaling up complex tasks through AI mediation. Despite the increasing attention to the macrotask phenomenon in crowdsourcing, there is a need to understand the processes, elements, and constraints underlying the infrastructural and behavioral aspects in such form of crowd work when involving collaboration. To this end, this paper provides a first attempt to characterize some of the research conducted in this direction to identify important paths for an agenda comprising key drivers, challenges, and prospects for integrating human-centered AI in collaborative crowdsourcing environments. © 2025 IEEE.

Abstract

Abstract

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