2 Search Results for "Arkor, Nathanael"

Document
DOI: 10.4230/LIPIcs.LICS.2026.65
A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on

Authors: Fabian Lenke, Stefan Milius, and Henning Urbat

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as λ-terms. One distinguishing feature of the presheaf-based perspective is its elegant syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, in the spirit of Fiore et al.’s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from a given action of a monoidal category on that category. We demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories but also yields notions of substitution tensor for nominal sets and their relatives, such as renaming sets. In the process, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of correspondences between them.
Cite as

Fabian Lenke, Stefan Milius, and Henning Urbat. A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 65:1-65:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lenke_et_al:LIPIcs.LICS.2026.65,
  author =	{Lenke, Fabian and Milius, Stefan and Urbat, Henning},
  title =	{{A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{65:1--65:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.65},
  URN =		{urn:nbn:de:0030-drops-268523},
  doi =		{10.4230/LIPIcs.LICS.2026.65},
  annote =	{Keywords: Substitution, Presheaves, Nominal Sets, Monoidal Category}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.30
Abstract Clones for Abstract Syntax

Authors: Nathanael Arkor and Dylan McDermott

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

Abstract
We give a formal treatment of simple type theories, such as the simply-typed λ-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed λ-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as β- and η-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.
Cite as

Nathanael Arkor and Dylan McDermott. Abstract Clones for Abstract Syntax. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{arkor_et_al:LIPIcs.FSCD.2021.30,
  author =	{Arkor, Nathanael and McDermott, Dylan},
  title =	{{Abstract Clones for Abstract Syntax}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{30:1--30:19},
  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.30},
  URN =		{urn:nbn:de:0030-drops-142686},
  doi =		{10.4230/LIPIcs.FSCD.2021.30},
  annote =	{Keywords: simple type theories, abstract clones, second-order abstract syntax, substitution, variable binding, presentations, free algebras, induction, logical relations}
}
  • Refine by Type
  • 2 Document/PDF

  • Refine by Publication Year
  • 1 2026
  • 1 2021

  • Refine by Author
  • 1 Arkor, Nathanael
  • 1 Lenke, Fabian
  • 1 McDermott, Dylan
  • 1 Milius, Stefan
  • 1 Urbat, Henning

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Theory of computation
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Monoidal Category
  • 1 Nominal Sets
  • 1 Presheaves
  • 1 Substitution
  • 1 abstract clones
  • 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