arXiv subjects

Éléonore Mangel

Publications and source records attributed to Éléonore Mangel.

3 recordsLinked to original sources

arXiv2026

Syntax and semantics of focalisation with relative monads and comonads

The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing effectful computation. On the semantics side, this corresponds to an axiomatic and polarised notion of model of computation stated in terms of adjunctions over non-associative categories. In this paper, we study the special and delicate cases of resource and effect modalities in a general intuitionistic and linear setting: an exponential comonad $!$ (refining $\square$) and a strong monad $\lozenge$. The starting point of our contribution is noticing that the completeness for a polarised syntax for $!$ and $\lozenge$ with respect to (co)monads in linear call-by-push-value models can be achieved if we move to relative (co)monads: more precisely, comonads relative to $\downarrow$ (the positive shift functor) for $!$ and monads relative to $\uparrow$ (the negative shift functor) for $\lozenge$. These specialisations of the concept of relative (co)monad to call-by-push-value adjunctions recently appeared. Yet the syntax we present arose from proof-theoretic consideration, without the link with relative (co)monads being noticed at the time. Our first remark is thus that (co)monads relative to a call-by-push-value adjunction have been motivated previously from a proof-theoretic perspective in the context of focalisation, which also provides a meta-language for these concepts in an effectful setting. We carry out the study of these modalities from the axiomatic, non-associative point of view. We recall the notion of adjunction over non-associative categories, and establish correspondence results between this notion of adjunction and that of relative adjunction. This correspondence is then extended to linear-non-linear and strong versions of adjunctions as needed to model $!$ and $\lozenge$.

cs.LO↗

arXiv2025

Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)

In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L-calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, we define a notion of adjunction between graph morphisms on non-associative categories, which we use to formulate polarized and non-associative notions of symmetric monoidal closed duploid and of dialogue duploid. We show that they provide a direct style counterpart to adjunction models: linear effect adjunctions for the (linear) call-by-push-value calculus and dialogue chiralities for linear continuations, respectively. In particular, we show that the syntax of the linear classical L-calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).

cs.LO↗

arXiv2023

Delooping the sign homomorphism in univalent mathematics

In univalent mathematics there are at least two equivalent ways to present the category of groups. Groups presented in their usual algebraic form are called abstract groups, and groups presented as pointed connected $1$-types are called concrete groups. Since these two descriptions of the category of groups are equivalent, we find that every algebraic group corresponds uniquely to a concrete group -- its delooping -- and that each abstract group homomorphisms corresponds uniquely to a pointed map between concrete groups. The $n$-th abstract symmetric group $S_n$ of all bijections $[n]\simeq [n]$, for instance, corresponds to the concrete group of all $n$-element types. The sign homomorphism from $S_n$ to $S_2$ should therefore correspond to a pointed map from the type $BS_n$ of all $n$-element types to the type $BS_2$ of all $2$-element types. Making use of the univalence axiom, we characterize precisely when a pointed map $BS_n\to_\ast BS_2$ is a delooping of the sign homomorphism. Then we proceed to give several constructions of the delooping of the sign homomorphism. Notably, the construction following a method of Cartier can be given without reference to the sign homomorphism. Our results are formalized in the agda-unimath library.

math.GR↗