Heterogeneous Substitution Systems Revisited

Ahrens, Benedikt; Matthes, Ralph

doi:10.4230/LIPIcs.TYPES.2015.2

License:

Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2015.2
URN: urn:nbn:de:0030-drops-84724
URL: https://drops.dagstuhl.de/opus/volltexte/2018/8472/

Ahrens, Benedikt ; Matthes, Ralph

Heterogeneous Substitution Systems Revisited

pdf-format:

LIPIcs-TYPES-2015-2.pdf (0.6 MB)

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}
}

15.03.2018

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: 15.03.2018

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:		15.03.2018