Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Ahrens, Benedikt; Matthes, Ralph http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-84724
URL:

;

Heterogeneous Substitution Systems Revisited

pdf-format:


Abstract

Matthes and Uustalu (TCS 327(1--2):155--174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems into a category and studying its properties, and we develop the proofs of the results of the cited paper and our new ones in UniMath, a recent library of univalent mathematics formalized in the Coq theorem prover.

BibTeX - Entry

@InProceedings{ahrens_et_al:LIPIcs:2018:8472,
  author =	{Benedikt Ahrens and Ralph Matthes},
  title =	{{Heterogeneous Substitution Systems Revisited}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{2:1--2:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Tarmo Uustalu},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8472},
  URN =		{urn:nbn:de:0030-drops-84724},
  doi =		{10.4230/LIPIcs.TYPES.2015.2},
  annote =	{Keywords: formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding}
}

Keywords: formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding
Seminar: 21st International Conference on Types for Proofs and Programs (TYPES 2015)
Issue date: 2018
Date of publication: 2018


DROPS-Home | Fulltext Search | Imprint Published by LZI