-
LibIQ: Toward Real-Time Spectrum Classification in O-RAN dApps
Authors:
Filippo Olimpieri,
Noemi Giustini,
Andrea Lacava,
Salvatore D'Oro,
Tommaso Melodia,
Francesca Cuomo
Abstract:
The O-RAN architecture is transforming cellular networks by adopting RAN softwarization and disaggregation concepts to enable data-driven monitoring and control of the network. Such management is enabled by RICs, which facilitate near-real-time and non-real-time network control through xApps and rApps. However, they face limitations, including latency overhead in data exchange between the RAN and…
▽ More
The O-RAN architecture is transforming cellular networks by adopting RAN softwarization and disaggregation concepts to enable data-driven monitoring and control of the network. Such management is enabled by RICs, which facilitate near-real-time and non-real-time network control through xApps and rApps. However, they face limitations, including latency overhead in data exchange between the RAN and RIC, restricting real-time monitoring, and the inability to access user plain data due to privacy and security constraints, hindering use cases like beamforming and spectrum classification. In this paper, we leverage the dApps concept to enable real-time RF spectrum classification with LibIQ, a novel library for RF signals that facilitates efficient spectrum monitoring and signal classification by providing functionalities to read I/Q samples as time-series, create datasets and visualize time-series data through plots and spectrograms. Thanks to LibIQ, I/Q samples can be efficiently processed to detect external RF signals, which are subsequently classified using a CNN inside the library. To achieve accurate spectrum analysis, we created an extensive dataset of time-series-based I/Q samples, representing distinct signal types captured using a custom dApp running on a 5G deployment over the Colosseum network emulator and an OTA testbed. We evaluate our model by deploying LibIQ in heterogeneous scenarios with varying center frequencies, time windows, and external RF signals. In real-time analysis, the model classifies the processed I/Q samples, achieving an average accuracy of approximately 97.8% in identifying signal types across all scenarios. We pledge to release both LibIQ and the dataset created as a publicly available framework upon acceptance.
△ Less
Submitted 27 May, 2025; v1 submitted 15 May, 2025;
originally announced May 2025.
-
Linearization via Rewriting (Long Version)
Authors:
Ugo Dal Lago,
Federico Olimpieri
Abstract:
We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its linearization. The calculus is shown to be normalizing and confluent. Noticeably, every strongly normalizable lambda-term can be represented by a type derivation. Th…
▽ More
We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its linearization. The calculus is shown to be normalizing and confluent. Noticeably, every strongly normalizable lambda-term can be represented by a type derivation. This is the first example of a system where the linearization process takes place internally, while remaining purely finitary and rewrite-based.
△ Less
Submitted 25 March, 2025; v1 submitted 6 March, 2025;
originally announced March 2025.
-
An Indexed Linear Logic for Idempotent Intersection Types (Long version)
Authors:
Flavien Breuvart,
Federico Olimpieri
Abstract:
Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an idempotent variant of Indexed Linear Logic. We give a fine-grained reformulation of the syntax by exposing implicit parameters and by unifying several operations on form…
▽ More
Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an idempotent variant of Indexed Linear Logic. We give a fine-grained reformulation of the syntax by exposing implicit parameters and by unifying several operations on formulae via the notion of base change. Idempotency is achieved by means of an appropriate subtyping relation. We carry on an in-depth study of indLL as a logic, showing how it determines a refinement of classical linear logic and establishing a terminating cut-elimination procedure. Cut-elimination is proved to be confluent up to an appropriate congruence induced by the subtyping relation.
△ Less
Submitted 15 February, 2024; v1 submitted 25 January, 2024;
originally announced January 2024.
-
Canonicity of Proofs in Constructive Modal Logic
Authors:
Matteo Acclavio,
Davide Catta,
Federico Olimpieri
Abstract:
In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction ru…
▽ More
In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction rules and we prove normalization and confluence for our calculus. We then provide a typing system in the style of focused proof systems allowing us to provide a unique proof for each term in normal form, and we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies.
△ Less
Submitted 30 July, 2023; v1 submitted 11 April, 2023;
originally announced April 2023.
-
Coherence by Normalization for Linear Multicategorical Structures
Authors:
Federico Olimpieri
Abstract:
We establish a formal correspondence between resource calculi an appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation and a structural equivalence.…
▽ More
We establish a formal correspondence between resource calculi an appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation and a structural equivalence. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms that live in the free multicategorical structures are the same whenever the normal forms of the associated terms are equal. As further application, we obtain syntactic proofs of Mac Lane's coherence theorems for (symmetric) monoidal categories.
△ Less
Submitted 27 July, 2023; v1 submitted 11 February, 2023;
originally announced February 2023.
-
From Thin Concurrent Games to Generalized Species of Structures (Extended Version)
Authors:
Pierre Clairambault,
Federico Olimpieri,
Hugo Paquet
Abstract:
Two families of denotational models have emerged from the semantic analysis of linear logic: dynamic models, typically presented as game semantics, and static models, typically based on a category of relations. In this paper we introduce a formal bridge between a dynamic model and a static model: the model of thin concurrent games and strategies, based on event structures, and the model of general…
▽ More
Two families of denotational models have emerged from the semantic analysis of linear logic: dynamic models, typically presented as game semantics, and static models, typically based on a category of relations. In this paper we introduce a formal bridge between a dynamic model and a static model: the model of thin concurrent games and strategies, based on event structures, and the model of generalized species of structures, based on distributors. A special focus of this paper is the two-dimensional nature of the dynamic-static relationship, which we formalize with double categories and bicategories.
In the first part of the paper, we construct a symmetric monoidal oplax functor from linear concurrent strategies to distributors. We highlight two fundamental differences between the two models: the composition mechanism, and the representation of resource symmetries. In the second part of the paper, we adapt established methods from game semantics (visible strategies, payoff structure) to enforce a tighter connection between the two models. We obtain a cartesian closed pseudofunctor, which we exploit to shed new light on recent results in the theory of the lambda-calculus.
△ Less
Submitted 19 July, 2024; v1 submitted 2 February, 2023;
originally announced February 2023.
-
On the Taylor expansion of $λ$-terms and the groupoid structure of their rigid approximants
Authors:
Federico Olimpieri,
Lionel Vaux Auclair
Abstract:
We show that the normal form of the Taylor expansion of a $λ$-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad hoc. We also introduce a groupoid of permutations…
▽ More
We show that the normal form of the Taylor expansion of a $λ$-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a nondeterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier's approach can be preserved in this setting.
△ Less
Submitted 5 January, 2022; v1 submitted 6 August, 2020;
originally announced August 2020.
-
Intersection Type Distributors
Authors:
Federico Olimpieri
Abstract:
We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian…
▽ More
We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.
△ Less
Submitted 5 May, 2021; v1 submitted 4 February, 2020;
originally announced February 2020.
-
Normalization, Taylor expansion and rigid approximation of $λ$-terms
Authors:
Federico Olimpieri
Abstract:
The aim of this work is to characterize three fundamental normalization proprieties in lambda-calculus trough the Taylor expansion of $ λ$-terms. The general proof strategy consists in stating the dependence of ordinary reduction strategies on their resource counterparts and in finding a convenient resource term in the Taylor expansion that behaves well under the considered kind of reduction.
The aim of this work is to characterize three fundamental normalization proprieties in lambda-calculus trough the Taylor expansion of $ λ$-terms. The general proof strategy consists in stating the dependence of ordinary reduction strategies on their resource counterparts and in finding a convenient resource term in the Taylor expansion that behaves well under the considered kind of reduction.
△ Less
Submitted 6 January, 2020;
originally announced January 2020.
