Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory

Benedikt Ahrens, Régis Spadotti

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

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öf type theory. Our results are mechanized in the proof assistant Coq.
Original languageEnglish
Title of host publication20th International Conference on Types for Proofs and Programs (TYPES 2014)
EditorsHugo Herbelin, Pierre Letouzey, Matthieu Sozeau
PublisherSchloss Dagstuhl
Pages1-26
Volume39
ISBN (Print)978-3-939897-88-0
DOIs
Publication statusPublished - 1 Oct 2015
Event20th International Conference on Types for Proofs and Programs (TYPES’14) - Paris, France
Duration: 12 May 201415 May 2014

Publication series

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

Conference

Conference20th International Conference on Types for Proofs and Programs (TYPES’14)
Country/TerritoryFrance
CityParis
Period12/05/1415/05/14

Keywords

  • relative comonad
  • Martin-Löf type theory
  • coinductive type
  • computer theorem proving

Fingerprint

Dive into the research topics of 'Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory'. Together they form a unique fingerprint.

Cite this