Search Results

Documents authored by Hirschowitz, Tom

Document
DOI: 10.4230/LIPIcs.FSCD.2020.12
Modules over Monads and Operational Semantics

Authors: André Hirschowitz, Tom Hirschowitz, and Ambroise Lafont

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

Abstract
This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as ̅λμ-calculus, π-calculus, Positive GSOS specifications, differential λ-calculus, and the big-step, simply-typed, call-by-value λ-calculus. Finally, we design a suitable notion of signature for transition monads.
Cite as

André Hirschowitz, Tom Hirschowitz, and Ambroise Lafont. Modules over Monads and Operational Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hirschowitz_et_al:LIPIcs.FSCD.2020.12,
  author =	{Hirschowitz, Andr\'{e} and Hirschowitz, Tom and Lafont, Ambroise},
  title =	{{Modules over Monads and Operational Semantics}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{12:1--12:23},
  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.12},
  URN =		{urn:nbn:de:0030-drops-123341},
  doi =		{10.4230/LIPIcs.FSCD.2020.12},
  annote =	{Keywords: Operational semantics, Category theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.16
Template Games, Simple Games, and Day Convolution

Authors: Clovis Eberhart, Tom Hirschowitz, and Alexis Laouar

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Template games [P.-A. Melliès, 2019] unify various approaches to game semantics, by exhibiting them as instances of a double-categorical variant of the slice construction. However, in the particular case of simple games [R. Harmer et al., 2007; C. Jacq and P.-A. Melliès, 2018], template games do not quite yield the standard (bi)category. We refine the construction using factorisation systems, obtaining as an instance a slight generalisation of simple games and strategies. This proves that template games have the descriptive power to capture combinatorial constraints defining well-known classes of games. Another instance is Day’s convolution monoidal structure on the category of presheaves over a strict monoidal category [B. Day, 1970], which answers a question raised in [C. Eberhart, 2018].
Cite as

Clovis Eberhart, Tom Hirschowitz, and Alexis Laouar. Template Games, Simple Games, and Day Convolution. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{eberhart_et_al:LIPIcs.FSCD.2019.16,
  author =	{Eberhart, Clovis and Hirschowitz, Tom and Laouar, Alexis},
  title =	{{Template Games, Simple Games, and Day Convolution}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.16},
  URN =		{urn:nbn:de:0030-drops-105237},
  doi =		{10.4230/LIPIcs.FSCD.2019.16},
  annote =	{Keywords: Game semantics, Day convolution, Categorical semantics}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.10
Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics

Authors: Clovis Eberhart and Tom Hirschowitz

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
Recent developments of game semantics have given rise to new models of concurrent languages. On the one hand, an approach based on string diagrams has given models of CCS and the pi-calculus, and on the other hand, Tsukada and Ong have designed a games model for a non-deterministic lambda-calculus. There is an obvious, shallow relationship between the two approaches, as they both define innocent strategies as sheaves for a Grothendieck topology embedding "views" into "plays". However, the notions of views and plays differ greatly between the approaches: Tsukada and Ong use notions from standard game semantics, while the authors of this paper use string diagrams. We here aim to bridge this gap by showing that even though the notions of plays, views, and innocent strategies differ, it is mostly a matter of presentation.
Cite as

Clovis Eberhart and Tom Hirschowitz. Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{eberhart_et_al:LIPIcs.CALCO.2017.10,
  author =	{Eberhart, Clovis and Hirschowitz, Tom},
  title =	{{Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.10},
  URN =		{urn:nbn:de:0030-drops-80407},
  doi =		{10.4230/LIPIcs.CALCO.2017.10},
  annote =	{Keywords: Concurrency, Sheaves, Presheaf models, Game Semantics}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.86
An Intensionally Fully-abstract Sheaf Model for pi

Authors: Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.
Cite as

Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An Intensionally Fully-abstract Sheaf Model for pi. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 86-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{eberhart_et_al:LIPIcs.CALCO.2015.86,
  author =	{Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},
  title =	{{An Intensionally Fully-abstract Sheaf Model for pi}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{86--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.86},
  URN =		{urn:nbn:de:0030-drops-55284},
  doi =		{10.4230/LIPIcs.CALCO.2015.86},
  annote =	{Keywords: concurrency, sheaves, causal models, games}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.226
Wild omega-Categories for the Homotopy Hypothesis in Type Theory

Authors: André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
In classical homotopy theory, the homotopy hypothesis asserts that the fundamental varpi-groupoid construction induces an equivalence between topological spaces and weak varpi-groupoids. In the light of Voevodsky's univalent foundations program, which puts forward an interpretation of types as topological spaces, we consider the question of transposing the homotopy hypothesis to type theory. Indeed such a transposition could stand as a new approach to specifying higher inductive types. Since the formalisation of general weak varpi-groupoids in type theory is a difficult task, we only take a first step towards this goal, which consists in exploring a shortcut through strict varpi-categories. The first outcome is a satisfactory type-theoretic notion of strict varpi-category, which has hsets of cells in all dimensions. For this notion, defining the 'fundamental strict varpi-category' of a type seems out of reach. The second outcome is an 'incoherently strict' notion of type-theoretic varpi-category, which admits arbitrary types of cells in all dimensions. These are the 'wild' varpi-categories of the title. They allow the definition of a 'fundamental wild varpi-category' map, which leads to our (partial) homotopy hypothesis for type theory (stating an adjunction, not an equivalence). All of our results have been formalised in the Coq proof assistant. Our formalisation makes systematic use of the machinery of coinductive types.
Cite as

André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 226-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hirschowitz_et_al:LIPIcs.TLCA.2015.226,
  author =	{Hirschowitz, Andr\'{e} and Hirschowitz, Tom and Tabareau, Nicolas},
  title =	{{Wild omega-Categories for the Homotopy Hypothesis in Type Theory}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{226--240},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.226},
  URN =		{urn:nbn:de:0030-drops-51669},
  doi =		{10.4230/LIPIcs.TLCA.2015.226},
  annote =	{Keywords: Homotopy Type theory; Omega-categories; Coinduction; Homotopy hypothesis}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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