首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory
  • 本地全文:下载
  • 作者:Benedikt Ahrens ; R{\'e}gis Spadotti
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:39
  • 页码:1-26
  • DOI:10.4230/LIPIcs.TYPES.2014.1
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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öf type theory. Our results are mechanized in the proof assistant Coq.
  • 关键词:relative comonad; Martin-L{\"o
国家哲学社会科学文献中心版权所有