Paper Info
Title
Heterogeneous substitution systems revisited.
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.
Year
DOI
Venue
2015
10.4230/LIPIcs.TYPES.2015.2
TYPES
DocType
Volume
Citations 
Conference
abs/1601.04299
0
PageRank 
References 
Authors
0.34
2
2
Name
Order
Citations
PageRank
Benedikt Ahrens1339.90
Ralph Matthes220121.67