Heterogeneous substitution systems revisited

Benedikt Ahrens; Ralph Matthes

doi:10.4230/LIPIcs.TYPES.2015.2

Heterogeneous substitution systems revisited

Benedikt Ahrens
, Ralph Matthes

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

93 Downloads (Pure)

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.

Original language	English
Title of host publication	21st International Conference on Types and Proofs and Programs - TYPES 2015 - Postproceedings
Editors	Tarmo Uustalu
Publisher	Schloss Dagstuhl
Pages	2:1 - 2:23
Number of pages	23
Volume	69
ISBN (Electronic)	978-3-95977-030-9
DOIs	https://doi.org/10.4230/LIPIcs.TYPES.2015.2
Publication status	Published - 16 Feb 2018
Event	21st International Conference on Types and Proofs and Programs (TYPES 2015) - Tallinn, Estonia Duration: 18 May 2015 → 21 May 2015

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl
Volume	69
ISSN (Electronic)	1868-8969

Conference

Conference	21st International Conference on Types and Proofs and Programs (TYPES 2015)
Country/Territory	Estonia
City	Tallinn
Period	18/05/15 → 21/05/15

Keywords

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

Access to Document

10.4230/LIPIcs.TYPES.2015.2Licence: Creative Commons: Attribution (CC BY)

Ahrens_Matthes_Heterogeneous_Substitution_SystemsFinal published version, 611 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

@inproceedings{ec60a2f97ed24a0da3fea851f66fb2c9,

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. ",

keywords = "formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding",

author = "Benedikt Ahrens and Ralph Matthes",

year = "2018",

month = feb,

day = "16",

doi = "10.4230/LIPIcs.TYPES.2015.2",

language = "English",

volume = "69",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl",

pages = "2:1 -- 2:23",

editor = "Tarmo Uustalu",

booktitle = "21st International Conference on Types and Proofs and Programs - TYPES 2015 - Postproceedings",

address = "Germany",

note = "21st International Conference on Types and Proofs and Programs (TYPES 2015) ; Conference date: 18-05-2015 Through 21-05-2015",

}

Ahrens, B & Matthes, R 2018, Heterogeneous substitution systems revisited. in T Uustalu (ed.), 21st International Conference on Types and Proofs and Programs - TYPES 2015 - Postproceedings. vol. 69, Leibniz International Proceedings in Informatics (LIPIcs), vol. 69, Schloss Dagstuhl, pp. 2:1 - 2:23, 21st International Conference on Types and Proofs and Programs (TYPES 2015), Tallinn, Estonia, 18/05/15. https://doi.org/10.4230/LIPIcs.TYPES.2015.2

Heterogeneous substitution systems revisited. / Ahrens, Benedikt; Matthes, Ralph.
21st International Conference on Types and Proofs and Programs - TYPES 2015 - Postproceedings. ed. / Tarmo Uustalu. Vol. 69 Schloss Dagstuhl, 2018. p. 2:1 - 2:23 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 69).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Heterogeneous substitution systems revisited

AU - Ahrens, Benedikt

AU - Matthes, Ralph

PY - 2018/2/16

Y1 - 2018/2/16

N2 - 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.

AB - 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.

KW - formalization of category theory

KW - nested datatypes

KW - Mendler-style recursion schemes

KW - representation of substitution in languages with variable binding

UR - https://arxiv.org/pdf/1601.04299.pdf

UR - https://www.scopus.com/pages/publications/85045452629

U2 - 10.4230/LIPIcs.TYPES.2015.2

DO - 10.4230/LIPIcs.TYPES.2015.2

M3 - Conference contribution

VL - 69

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 2:1 - 2:23

BT - 21st International Conference on Types and Proofs and Programs - TYPES 2015 - Postproceedings

A2 - Uustalu, Tarmo

PB - Schloss Dagstuhl

T2 - 21st International Conference on Types and Proofs and Programs (TYPES 2015)

Y2 - 18 May 2015 through 21 May 2015

ER -

Heterogeneous substitution systems revisited

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this