Search Results

Documents authored by Galal, Zeinab

Document
DOI: 10.4230/LIPIcs.CONCUR.2026.29
Coinductive Reasoning for Parametrized Functors and Monads

Authors: Ugo Dal Lago and Zeinab Galal

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract
Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.
Cite as

Ugo Dal Lago and Zeinab Galal. Coinductive Reasoning for Parametrized Functors and Monads. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 29:1-29:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.CONCUR.2026.29,
  author =	{Dal Lago, Ugo and Galal, Zeinab},
  title =	{{Coinductive Reasoning for Parametrized Functors and Monads}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{29:1--29:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.29},
  URN =		{urn:nbn:de:0030-drops-273598},
  doi =		{10.4230/LIPIcs.CONCUR.2026.29},
  annote =	{Keywords: categorical semantics, parametrized monads, effects, relations, lax extensions, behavioral equivalence, coalgebra, global state}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.31
A Combinatorial Approach to Higher-Order Structure for Polynomial Functors

Authors: Marcelo Fiore, Zeinab Galal, and Hugo Paquet

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Polynomial functors are categorical structures used in a variety of applications across theoretical computer science; for instance, in database theory, denotational semantics, functional programming, and type theory. A well-known problem is that the bicategory of finitary polynomial functors between categories of indexed sets is not cartesian closed, despite its success and influence on denotational models and linear logic. This paper introduces a formal bridge between the model of finitary polynomial functors and the combinatorial theory of generalised species of structures. Our approach consists in viewing finitary polynomial functors as free analytic functors, which correspond to free generalised species. In order to systematically consider finitary polynomial functors from this combinatorial perspective, we study a model of groupoids with additional logical structure; this is used to constrain the generalised species between them. The result is a new cartesian closed bicategory that embeds finitary polynomial functors.
Cite as

Marcelo Fiore, Zeinab Galal, and Hugo Paquet. A Combinatorial Approach to Higher-Order Structure for Polynomial Functors. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fiore_et_al:LIPIcs.FSCD.2022.31,
  author =	{Fiore, Marcelo and Galal, Zeinab and Paquet, Hugo},
  title =	{{A Combinatorial Approach to Higher-Order Structure for Polynomial Functors}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.31},
  URN =		{urn:nbn:de:0030-drops-163129},
  doi =		{10.4230/LIPIcs.FSCD.2022.31},
  annote =	{Keywords: Bicategorical models, denotational semantics, stable domain theory, linear logic, polynomial functors, species of structures, groupoids}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.10
A Bicategorical Model for Finite Nondeterminism

Authors: Zeinab Galal

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Finiteness spaces were introduced by Ehrhard as a refinement of the relational model of linear logic. A finiteness space is a set equipped with a class of finitary subsets which can be thought of being subsets that behave like finite sets. A morphism between finiteness spaces is a relation that preserves the finitary structure. This model provided a semantics for finite non-determism and it gave a semantical motivation for differential linear logic and the syntactic notion of Taylor expansion. In this paper, we present a bicategorical extension of this construction where the relational model is replaced with the model of generalized species of structures introduced by Fiore et al. and the finiteness property now relies on finite presentability.
Cite as

Zeinab Galal. A Bicategorical Model for Finite Nondeterminism. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{galal:LIPIcs.FSCD.2021.10,
  author =	{Galal, Zeinab},
  title =	{{A Bicategorical Model for Finite Nondeterminism}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.10},
  URN =		{urn:nbn:de:0030-drops-142487},
  doi =		{10.4230/LIPIcs.FSCD.2021.10},
  annote =	{Keywords: Differential linear logic, Species of structures, Finiteness, Bicategorical semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.16
A Profunctorial Scott Semantics

Authors: Zeinab Galal

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
In this paper, we study the bicategory of profunctors with the free finite coproduct pseudo-comonad and show that it constitutes a model of linear logic that generalizes the Scott model. We formalize the connection between the two models as a change of base for enriched categories which induces a pseudo-functor that preserves all the linear logic structure. We prove that morphisms in the co-Kleisli bicategory correspond to the concept of strongly finitary functors (sifted colimits preserving functors) between presheaf categories. We further show that this model provides solutions of recursive type equations which provides 2-dimensional models of the pure lambda calculus and we also exhibit a fixed point operator on terms.
Cite as

Zeinab Galal. A Profunctorial Scott Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{galal:LIPIcs.FSCD.2020.16,
  author =	{Galal, Zeinab},
  title =	{{A Profunctorial Scott Semantics}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.16},
  URN =		{urn:nbn:de:0030-drops-123387},
  doi =		{10.4230/LIPIcs.FSCD.2020.16},
  annote =	{Keywords: Linear Logic, Scott Semantics, Profunctors}
}

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact