arXiv subjects

Davide Trotta

Publications and source records attributed to Davide Trotta.

At least 19 recordsLinked to original sources

arXiv2026

NTL-amplified cryogenic light detectors with optically transparent electrodes

The Neganov-Trofimov-Luke (NTL) effect is used by experiments based on cryogenic detectors to boost the sensitivity of light-sensitive devices down to a few optical photons. In this work we introduce a silicon light-detector technology that implements NTL amplification at millikelvin temperatures using transparent indium-tin-oxide (ITO) electrodes. The ITO electrodes enable an electric field perpendicular to the wafer surface, mitigating surface charge recombination, and thanks to their optical properties, simultaneously serve as an anti-reflective coating. By combining these two functions in a single element, the fabrication process is simplified, yielding more robust and cost-effective devices. We report on the production and characterization of the first batch of these detectors. We performed a room-temperature characterization of the ITO electrodes, verifying the structural and optical characteristics of the deposited electrodes. We then operated 2 of these devices as cryogenic calorimeters at millikelvin temperatures. Finally, we develop a consistent analytical model for the NTL gain for both ionizing particles and optical photons, successfully describing the gain dependence on the NTL bias and explicitly accounting for the partial electrode coverage of the device surface.

physics.ins-det↗

arXiv2025

An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction

Localic and realizability toposes are two central classes of toposes in categorical logic, both arising through the Hyland-Johnstone-Pitts tripos-to-topos construction. We investigate their shared geometric features by providing an algebraic abstraction of the notions of localic presheaves, sheafification and their connection to supercompactification of a locale via an instance of the Comparison Lemma. This can be applied to a broad class of toposes obtained to the tripos-to-topos constructions, including all those generated from a tripos based on the classical category of ZFC-sets. These results provide a unified geometric framework for understanding localic and realizability toposes.

math.CT↗

arXiv2025

Between Markov and restriction. Two more monads on categories for relations

The study of categories abstracting the structural properties of relations has been extensively developed over the years, resulting in a rich and diverse body of work. In a previous paper we offered a survey providing a modern presentation of these ``categories for relations'' as instances of gs-monoidal categories, showing how they arise as Kleisli categories of suitable symmetric monoidal monads. The end result was a taxonomy that organised numerous related concepts in the literature, including in particular Markov and restriction categories. This paper further enriches the taxonomy: it proposes two categories that are once more instances of gs-monoidal categories, yet more abstract than Markov and restriction categories. They are characterised by an axiomatic notion of mass and domain of an arrow, the latter one of the key ingredients of restriction categories, which generalises the domain of partial functions. The paper then introduces mass and domain preserving monads, proving that the associated Kleisli categories in fact preserve the corresponding equations and that these monads arise naturally for the categories of semiring-weighted relations.

cs.LO↗

arXiv2025

A topos for extended Weihrauch degrees

Weihrauch reducibility is a notion of reducibility between computational problems that is useful to calibrate the uniform computational strength of a multivalued function. It complements the analysis of mathematical theorems done in reverse mathematics, as multi-valued functions on represented spaces can be considered as realizers of theorems in a natural way. Despite the rich literature and the relevance of the applications of category theory in logic and realizability, actually there are just a few works starting to study the Weihrauch reducibility from a categorical point of view. The main purpose of this work is to provide a full categorical account to the notion of extended Weihrauch reducibility introduced by A. Bauer, which generalizes the original notion of Weihrauch reducibility. In particular, we present a tripos and a topos for extended Weihrauch degrees. We start by defining a new tripos, abstracting the notion of extended Weihrauch degrees, and then we apply the tripos-to-topos construction to obtain the desired topos. Then we show that the Kleene-Vesley topos is a topos of $j$-sheaves for a certain Lawvere-Tierney topology over the topos of extended Weihrauch degrees.

math.CT↗

arXiv2025

A taxonomy of categories for relations

The study of categories that abstract the structural properties of relations has been extensively developed over the years, resulting in a rich and diverse body of work. This paper strives to provide a modern presentation of these ``categories for relations'', including their enriched version, further showing how they arise as Kleisli categories of symmetric monoidal monads. The resulting taxonomy aims at bringing clarity and organisation to the many related concepts and frameworks occurring in the literature.

math.CT↗

arXiv2025

Categorifying computable reducibilities

This paper presents categorical formulations of Turing, Medvedev, Muchnik, and Weihrauch reducibilities in Computability Theory, utilizing Lawvere doctrines. While the first notions lend themselves to a smooth categorical presentation, essentially dualizing the traditional idea of realizability doctrines, Weihrauch reducibility and its extensions to represented and multi-represented spaces require a separate investigation. Our abstract analysis of these concepts highlights a shared characteristic among all these reducibilities. Specifically, we demonstrate that all these doctrines stemming from computability concepts can be proven to be instances of completions of quantifiers for doctrines, analogous to what occurs for doctrines for realizability. As a corollary of these results, we will be able to formally compare Weihrauch reducibility with the dialectica doctrine constructed from a doctrine representing Turing degrees.

math.LO↗

arXiv2024

Skolem, Gödel, and Hilbert fibrations

Grothendieck fibrations are fundamental in capturing the concept of dependency, notably in categorical semantics of type theory and programming languages. A relevant instance are Dialectica fibrations which generalise Gödel's Dialectica proof interpretation and have been widely studied in recent years. We characterise when a given fibration is a generalised, dependent Dialectica fibration, namely an iterated completion of a fibration by dependent products and sums (along a given class of display maps). From a technical perspective, we complement the work of Hofstra on Dialectica fibrations by an internal viewpoint, categorifying the classical notion of quantifier-freeness. We also generalise both Hofstra's and Trotta et al.'s work on Gödel fibrations to the dependent case, replacing the class of cartesian projections in the base category by arbitrary display maps. We discuss how this recovers a range of relevant examples in categorical logic and proof theory. Moreover, as another instance, we introduce Hilbert fibrations, providing a categorical understanding of Hilbert's $ε$- and $τ$-operators well-known from proof theory.

math.CT↗

arXiv2024

Compositional theories for host-core languages

Linear type theories, of various types and kinds, are of fundamental importance in most programming language research nowadays. In this paper we describe an extension of Benton's Linear-Non-Linear type theory and model for which we can prove some extra properties that make the system better behaved as far as its theory is concerned. We call this system the host-core type theory. The syntax of a host-core language is split into two parts, representing respectively a host language H and a core language C, embedded in H. This idea, derived from Benton's Linear-Non-Linear formulation of Linear Logic, allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms. The host-core style can be viewed as a simplified notion of multi-language programming, the process of software development in a heterogeneous programming language. In this paper, we present the typed calculus HC, a minimal and flexible host-core system that captures and standardizes common properties of an ideal class of host-core languages. We provide a denotational model in terms of enriched categories and we state a strong correspondence between syntax and semantics through the notion of internal language. The latter result provides some useful characterizations of host-core style, otherwise difficult to obtain. We also discuss some concrete instances, extensions and specializations of the system HC.

cs.LO↗

arXiv2024

Quotients, pure existential completions and arithmetic universes

We provide a new description of Joyal's arithmetic universes through a characterization of the exact and regular completions of pure existential completions. We show that the regular and exact completions of the pure existential completion of an elementary doctrine $P$ are equivalent to the $\mathsf{reg}/\mathsf{lex}$ and $\mathsf{ex}/\mathsf{lex}$-completions, respectively, of the category of predicates of $P$. This result generalizes a previous one by the first author with F. Pasquali and G. Rosolini about doctrines equipped with Hilbert's $ε$-operators. Thanks to this characterization, each arithmetic universe in the sense of Joyal can be seen as the exact completion of the pure existential completion of the doctrine of predicates of its Skolem theory. In particular, the initial arithmetic universe in the standard category of ZFC-sets turns out to be the completion with exact quotients of the doctrine of recursively enumerable predicates.

math.CT↗

arXiv2024

When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines

Fo-bicategories are a categorification of Peirce's calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere's hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.

math.CT↗

arXiv2023

From Gs-monoidal to Oplax Cartesian Categories: Constructions and Functorial Completeness

Originally introduced in the context of the algebraic approach to term graph rewriting, the notion of gs-monoidal category has surfaced a few times under different monikers in the last decades. They can be thought of as symmetric monoidal categories whose arrows are generalised relations, with enough structure to talk about domains and partial functions, but less structure than cartesian bicategories. The aim of this paper is threefold. The first goal is to extend the original definition of gs-monoidality by enriching it with a preorder on arrows, giving rise to what we call oplax cartesian categories. Second, we show that (preorder-enriched) gs-monoidal categories naturally arise both as Kleisli categories and as span categories, and the relation between the resulting formalisms is explored. Finally, we present two theorems concerning Yoneda embeddings on the one hand and functorial completeness on the other, the latter inducing a completeness result also for lax functors from oplax cartesian categories to $\mathbf{Rel}$.

cs.LO↗

arXiv2023

Weakly Markov categories and weakly affine monads

Introduced in the 1990s in the context of the algebraic approach to graph rewriting, gs-monoidal categories are symmetric monoidal categories where each object is equipped with the structure of a commutative comonoid. They arise for example as Kleisli categories of commutative monads on cartesian categories, and as such they provide a general framework for effectful computation. Recently proposed in the context of categorical probability, Markov categories are gs-monoidal categories where the monoidal unit is also terminal, and they arise for example as Kleisli categories of commutative affine monads, where affine means that the monad preserves the monoidal unit. The aim of this paper is to study a new condition on the gs-monoidal structure, resulting in the concept of weakly Markov categories, which is intermediate between gs-monoidal categories and Markov ones. In a weakly Markov category, the morphisms to the monoidal unit are not necessarily unique, but form a group. As we show, these categories exhibit a rich theory of conditional independence for morphisms, generalising the known theory for Markov categories. We also introduce the corresponding notion for commutative monads, which we call weakly affine, and for which we give two equivalent characterisations. The paper argues that these monads are relevant to the study of categorical probability. A case at hand is the monad of finite non-zero measures, which is weakly affine but not affine. Such structures allow to investigate probability without normalisation within an elegant categorical framework.

math.CT↗

arXiv2023

On categorical structures arising from implicative algebras: from topology to assemblies

Implicative algebras have been recently introduced by Miquel in order to provide a unifying notion of model, encompassing the most relevant and used ones, such as realizability (both classical and intuitionistic), and forcing. In this work, we initially approach implicative algebras as a generalization of locales, and we extend several topological-like concepts to the realm of implicative algebras, accompanied by various concrete examples. Then, we shift our focus to viewing implicative algebras as a generalization of partial combinatory algebras. We abstract the notion of a category of assemblies, partition assemblies, and modest sets to arbitrary implicative algebras, and thoroughly investigate their categorical properties and interrelationships.

math.CT↗

arXiv2023

Specification and verification of a linear-time logic for graph transformation

We present a first-order linear-time temporal logic for reasoning about the evolution of directed graphs. Its semantics is based on the counterpart paradigm, thus allowing our logic to represent the creation, duplication, merging, and deletion of elements of a graph as well as how its topology changes over time. We then introduce a positive normal forms presentation, thus simplifying the actual process of verification. We provide the syntax and semantics of our logics with a computer-assisted formalisation using the proof assistant Agda, and we round up the paper by highlighting the crucial aspects of our formalisation and the practical use of quantified temporal logics in a constructive proof assistant.

cs.LO↗

arXiv2022

Dialectica Principles via Gödel Doctrines

Gödel's Dialectica interpretation was conceived as a tool to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic in the 40s. In recent years, several proof-theoretic transformations, based on Gödel's Dialectica interpretation, have been used systematically to extract new content from classical proofs, following a suggestion of Kreisel. Thus, the interpretation has found new relevant applications in several areas of mathematics and computer science. Several authors have explained the Dialectica interpretation in categorical terms. In our previous work, we introduced an intrinsic categorical presentation of the Dialectica construction via a generalisation of Hofstra's work, using the notion of Gödel fibration and its proof-irrelevant version, a Gödel doctrine. The key idea is that Gödel fibrations can be thought of as fibrations generated by some basic elements playing the role of quantifier-free elements. This categorification of quantifier-free elements is crucial not only to show that our notion of Gödel fibration is equivalent to Hofstra's Dialectica fibration in the appropriate way, but also to show how Gödel doctrines embody the main logical features of the Dialectica Interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded by Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely Markov Principle and the Independence of Premise principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight correspondence between the logical system and the categorical framework. Finally, to complete our analysis, we characterise categories obtained as results of the tripos-to-topos of Hyland, Johnstone and Pitts applied to Gödel doctrines.

math.CT↗

arXiv2022

A Presheaf Semantics for Quantified Temporal Logics

Temporal logics stands for a widely adopted family of formalisms for the verification of computational devices, enriching propositional logics by operators predicating on the step-wise behaviour of a system. Its quantified extensions allow to reason on the properties of the individual components of the system at hand. The expressiveness of the resulting logics poses problems in correctly identifying a semantics that exploit its features without resorting to the imposition of restrictions on the acceptable behaviours. In this paper we address this issue by means of counterpart models and relational presheaves.

cs.LO↗

arXiv2021

Generalized existential completions and their regular and exact completions

This paper aims to apply the tool of generalized existential completions of conjunctive doctrines, concerning a class $Λ$ of morphisms of their base category, to deepen the study of regular and exact completions of existential elementary Lawvere's doctrines. After providing a characterization of generalized existential completions, we observe that both the subobjects doctrine $\mathrm{Sub}_{C}$ and the weak subobjects doctrine $Ψ_{\mathcal{C}}$ of a category $\mathcal{C}$ with finite limits are generalized existential completions of the constant true doctrine, the first along the class of all the monomorphisms of $\mathcal{C}$ while the latter along all the morphisms of $\mathcal{C}$. We then name full existential completion a generalized completion of a conjunctive doctrine along the class of all the morphisms of its base. From this we immediately deduce that both the regular and the exact completion of a finite limit category are regular and exact completions of full existential doctrines since it is known that both the regular completion $(\mathcal{D})_{ reg / lex}$ and the exact completion $(\mathcal{D})_{ex / lex}$ of a finite limit category $\mathcal{D}$ are respectively the regular completion $\mathrm{Reg}(Ψ_{\mathcal{D}})$ and the exact completion $\mathcal{T}_{Ψ_{\mathcal{D}}}$ (as an instance of the tripos-to-topos construction) of the weak subobjects doctrine $Ψ_{\mathcal{D}}$ of $\mathcal{D}$. Here we prove that the condition of being a generic full existential completion is also sufficient to produce a regular/exact completion equivalent to a regular/exact completion of a finite limit category. Then, we show more specialized characterizations from which we derive known results as well as remarkable examples of exact completions of full existential completions, including all realizability toposes and supercoherent localic toposes.

math.CT↗

arXiv2021

Dialectica Logical Principles

Gödel's Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theoretic transformations (so-called proof interpretations) that are based on Gödel's Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on Gödel fibrations, we present a (hyper)doctrine characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that we derive in the category theory the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra. This requires extra logical principles, going beyond intuitionistic logic, Markov's Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. This tight correspondence should come handy not only when discussing the applications of the Dialectica already known, like its use to extract computational content from (some) classical theorems (proof mining), its use to help to model specific abstract machines, etc. but also to help devise new applications.

math.CT↗