Heterogeneous substitution systems revisited

Benedikt Ahrens, Ralph Matthes

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)
33 Downloads (Pure)


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.
Original languageEnglish
Title of host publication21st International Conference on Types and Proofs and Programs - TYPES 2015 - Postproceedings
EditorsTarmo Uustalu
PublisherSchloss Dagstuhl
Pages2:1 - 2:23
Number of pages23
ISBN (Electronic)978-3-95977-030-9
Publication statusPublished - 16 Feb 2018
Event21st International Conference on Types and Proofs and Programs (TYPES 2015) - Tallinn, Estonia
Duration: 18 May 201521 May 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl
ISSN (Electronic)1868-8969


Conference21st International Conference on Types and Proofs and Programs (TYPES 2015)


  • formalization of category theory
  • nested datatypes
  • Mendler-style recursion schemes
  • representation of substitution in languages with variable binding


Dive into the research topics of 'Heterogeneous substitution systems revisited'. Together they form a unique fingerprint.

Cite this