Terminal semantics for codata types in intensional Martin-L\"of type theory

DOI10.4230/LIPICS.TYPES.2014.1zbMath1367.68204arXiv1401.1053OpenAlexW2963721512MaRDI QIDQ5277969

Régis Spadotti, Benedikt Ahrens

Publication date: 12 July 2017

Abstract: In this work, we study the notions of relative comonad and comodule over a relative comonad, and use these notions to give a terminal coalgebra semantics for the coinductive type families of streams and of infinite triangular matrices, respectively, in intensional Martin-L"of type theory. Our results are mechanized in the proof assistant Coq.

Full work available at URL: https://arxiv.org/abs/1401.1053

zbMATH Keywords

Martin-Löf type theorycomputer theorem provingcoinductive typerelative comonad

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Eilenberg-Moore and Kleisli constructions for monads (18C20)

Related Items (2)

Linearity and uniqueness: an entente cordiale ⋮ The formal theory of relative monads

Uses Software

• Unnamed Item

This page was built for publication: Terminal semantics for codata types in intensional Martin-L\"of type theory