8 Search Results for "Hirschowitz, Tom"

Document
DOI: 10.4230/LIPIcs.TYPES.2023.3
Categorical Models of Subtyping

Authors: Greta Coraglia and Jacopo Emmenegger

Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)

Abstract
Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context - and for each type a set of terms of said type. This is the case for categories with families, categories with attributes, and natural models; in particular, all of them can be traced back to certain discrete Grothendieck fibrations. We extend this intuition to the case of general, not necessarily discrete, fibrations, so that over a given context one has not only a set but a category of types. We argue that the added structure can be attributed to a notion of subtyping that shares many features with that of coercive subtyping, in the sense that it is the product of thinking about subtyping as an abbreviation mechanism: we say that a given type A' is a subtype of A if there is a unique coercion from A' to A. Whenever we need a term of type A, then, it suffices to have a term of type A', which we can "plug-in" into A. For this version of subtyping we provide rules, coherences, and explicit models, and we compare and contrast it to coercive subtyping as introduced by Z. Luo and others. We conclude by suggesting how the tools we present can be employed in finding appropriate rules relating subtyping and certain type constructors.
Cite as

Greta Coraglia and Jacopo Emmenegger. Categorical Models of Subtyping. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{coraglia_et_al:LIPIcs.TYPES.2023.3,
  author =	{Coraglia, Greta and Emmenegger, Jacopo},
  title =	{{Categorical Models of Subtyping}},
  booktitle =	{29th International Conference on Types for Proofs and Programs (TYPES 2023)},
  pages =	{3:1--3:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-332-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{303},
  editor =	{Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.3},
  URN =		{urn:nbn:de:0030-drops-204811},
  doi =		{10.4230/LIPIcs.TYPES.2023.3},
  annote =	{Keywords: dependent types, subtyping, coercive subtyping, categorical semantics, categories with families, monad}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.25
Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories

Authors: Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens

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

Abstract
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation. Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multi-sorted binding signature, say Σ. First, we provide sufficient criteria for Σ to generate a language of possibly infinite terms, through ω-continuity. Second, we construct a monadic substitution operation for the language generated by Σ. A cornerstone in this construction is a mild generalization of the notion of heterogeneous substitution systems developed by Matthes and Uustalu; such a system encapsulates the necessary corecursion scheme for implementing substitution. The results are formalized in the Coq proof assistant, through the UniMath library of univalent mathematics.
Cite as

Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{matthes_et_al:LIPIcs.FSCD.2024.25,
  author =	{Matthes, Ralph and Wullaert, Kobe and Ahrens, Benedikt},
  title =	{{Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{25:1--25:22},
  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.25},
  URN =		{urn:nbn:de:0030-drops-203540},
  doi =		{10.4230/LIPIcs.FSCD.2024.25},
  annote =	{Keywords: Non-wellfounded syntax, Substitution, Monoidal categories, Actegories, Tensorial strength, Proof assistant Coq, UniMath library}
}
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.CSL.2020.31
Separation and Renaming in Nominal Sets

Authors: Joshua Moerman and Jurriaan Rot

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.
Cite as

Joshua Moerman and Jurriaan Rot. Separation and Renaming in Nominal Sets. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{moerman_et_al:LIPIcs.CSL.2020.31,
  author =	{Moerman, Joshua and Rot, Jurriaan},
  title =	{{Separation and Renaming in Nominal Sets}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.31},
  URN =		{urn:nbn:de:0030-drops-116744},
  doi =		{10.4230/LIPIcs.CSL.2020.31},
  annote =	{Keywords: Nominal sets, Separated product, Adjunction, Automata, Coalgebra}
}
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}
}
  • Refine by Author
  • 5 Hirschowitz, Tom
  • 3 Eberhart, Clovis
  • 2 Hirschowitz, André
  • 1 Ahrens, Benedikt
  • 1 Coraglia, Greta
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Categorical semantics
  • 2 Theory of computation → Type theory
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 1 Actegories
  • 1 Adjunction
  • 1 Automata
  • 1 Categorical semantics
  • 1 Category theory
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 2 2015
  • 2 2020
  • 2 2024
  • 1 2017
  • 1 2019

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