3 Search Results for "Saville, Philip"

Document
DOI: 10.4230/LIPIcs.FSCD.2025.10
Categorical Continuation Semantics for Concurrency

Authors: Flavien Breuvart and Hugo Paquet

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Continuation semantics for simple programming languages can be axiomatized as a dialogue category: a symmetric monoidal category equipped with a negation operation. This axiomatization makes clear the relationship between game semantics, CPS transformations, and continuation monads. In this paper we extend dialogue categories with 2-categorical structure and concurrent primitives. This is inspired by a recent analysis of concurrency based on 2-categorical monads. We show that the fine-grained structure of dialogue categories, not generally available in other semantic models, can be exploited to give a type to concurrent primitives join and fork. Our main theorem is that this simple axiomatization induces a concurrent continuation 2-monad. We also show that this framework is expressive beyond call-by-value monadic programming. The definitions in this paper are illustrated by concrete constructions in concurrent game semantics, and our results give a formal categorical basis for concurrent strategies. From a more practical perspective, our approach suggests a candidate target language for linear CPS transformations of concurrent programming languages.
Cite as

Flavien Breuvart and Hugo Paquet. Categorical Continuation Semantics for Concurrency. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2025.10,
  author =	{Breuvart, Flavien and Paquet, Hugo},
  title =	{{Categorical Continuation Semantics for Concurrency}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.10},
  URN =		{urn:nbn:de:0030-drops-236251},
  doi =		{10.4230/LIPIcs.FSCD.2025.10},
  annote =	{Keywords: denotational semantics, 2-categories, concurrency, continuations, game semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.14
Two-Dimensional Kripke Semantics I: Presheaves

Authors: G. A. Kavvos

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.
Cite as

G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kavvos:LIPIcs.FSCD.2024.14,
  author =	{Kavvos, G. A.},
  title =	{{Two-Dimensional Kripke Semantics I: Presheaves}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.14},
  URN =		{urn:nbn:de:0030-drops-203438},
  doi =		{10.4230/LIPIcs.FSCD.2024.14},
  annote =	{Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.16
List Objects with Algebraic Structure

Authors: Marcelo Fiore and Philip Saville

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We introduce and study the notion of list object with algebraic structure. The first key aspect of our development is that the notion of list object is considered in the context of monoidal structure; the second key aspect is that we further equip list objects with algebraic structure in this setting. Within our framework, we observe that list objects give rise to free monoids and moreover show that this remains so in the presence of algebraic structure. In addition, we provide a basic theory explicitly describing as an inductively defined object such free monoids with suitably compatible algebraic structure in common practical situations. This theory is accompanied by the study of two technical themes that, besides being of interest in their own right, are important for establishing applications. These themes are: parametrised initiality, central to the universal property defining list objects; and approaches to algebraic structure, in particular in the context of monoidal theories. The latter leads naturally to a notion of nsr (or near semiring) category of independent interest. With the theoretical development in place, we touch upon a variety of applications, considering Natural Numbers Objects in domain theory, giving a universal property for the monadic list transformer, providing free instances of algebraic extensions of the Haskell Monad type class, elucidating the algebraic character of the construction of opetopes in higher-dimensional algebra, and considering free models of second-order algebraic theories.
Cite as

Marcelo Fiore and Philip Saville. List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fiore_et_al:LIPIcs.FSCD.2017.16,
  author =	{Fiore, Marcelo and Saville, Philip},
  title =	{{List Objects with Algebraic Structure}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.16},
  URN =		{urn:nbn:de:0030-drops-77262},
  doi =		{10.4230/LIPIcs.FSCD.2017.16},
  annote =	{Keywords: list object, free monoid, strong monad, (cartesian, linear, and second-order) algebraic theory, near semiring, Haskell Monad type class, opetope}
}
  • Refine by Type
  • 3 Document/PDF

  • Refine by Publication Year
  • 1 2025
  • 1 2024
  • 1 2017

  • Refine by Author
  • 1 Breuvart, Flavien
  • 1 Fiore, Marcelo
  • 1 Kavvos, G. A.
  • 1 Paquet, Hugo
  • 1 Saville, Philip

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Categorical semantics
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Linear logic
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 1 (cartesian
  • 1 2-categories
  • 1 Haskell Monad type class
  • 1 Kripke semantics
  • 1 and second-order) algebraic theory
  • Show More...

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