Type Theory based on Dependent Inductive and Coinductive Types

DOI10.1145/2933575.2934514zbMath1394.03007arXiv1605.02206OpenAlexW3099982020MaRDI QIDQ4635888

Henning Basold, Herman Geuvers

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

fibrationsinductive typesdependent typescoinductive types

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Categorical logic, topoi (03G30)

Related Items (6)

Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Unnamed Item ⋮ Undecidability of equality for codata types

This page was built for publication: Type Theory based on Dependent Inductive and Coinductive Types