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

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

Authors

Colleges, School and Institutes

External organisations

  • Institut de Recherche en Informatique de Toulouse Université Paul Sabatier, Toulouse, France

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.

Details

Original languageEnglish
Title of host publication20th International Conference on Types for Proofs and Programs (TYPES 2014)
EditorsHugo Herbelin, Pierre Letouzey, Matthieu Sozeau
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)
CountryFrance
CityParis
Period12/05/1415/05/14

Keywords

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