@inproceedings{23322642974d47d0b206edd8dc129349,
title = "Terminal Semantics for Codata Types in Intensional Martin-L{\"o}f Type Theory",
abstract = "We study the notions of relative comonad and comodule over a relative comonad. We use these notions to give categorical semantics for the coinductive type families of streams and of infinite triangular matrices and their respective cosubstitution operations in intensional Martin-L{\"o}f type theory. Our results are mechanized in the proof assistant Coq.",
keywords = "relative comonad, Martin-L{\"o}f type theory, coinductive type, computer theorem proving",
author = "Benedikt Ahrens and R{\'e}gis Spadotti",
year = "2015",
month = oct,
day = "1",
doi = "10.4230/LIPIcs.TYPES.2014.1",
language = "English",
isbn = "978-3-939897-88-0",
volume = "39",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl",
pages = "1--26",
editor = "{ Herbelin}, Hugo and Pierre Letouzey and Matthieu Sozeau",
booktitle = "20th International Conference on Types for Proofs and Programs (TYPES 2014)",
address = "Germany",
note = "20th International Conference on Types for Proofs and Programs (TYPES{\textquoteright}14) ; Conference date: 12-05-2014 Through 15-05-2014",
}