Type Theory based on Dependent Inductive and Coinductive Types

DOI10.1145/2933575.2934514zbMATH Open1394.03007arXiv1605.02206OpenAlexW3099982020MaRDI QIDQ4635888FDOQ4635888

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)

Abstract: We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For example, all well-known basic types and type formers that are needed for using this type theory as a logic are definable: propositional connectives, like falsity, conjunction, disjunction, and function space, dependent function space, existential quantification, equality, natural numbers, vectors etc. The reduction relation on terms consists solely of a rule for recursion and a rule for corecursion. The reduction relations for well-known types arise from that. To further support the introduction of this new type theory, we also prove fundamental properties of its term calculus. Most importantly, we prove subject reduction and strong normalisation of the reduction relation, which gives computational meaning to the terms. The presented type theory is based on ideas from categorical logic that have been investigated before by the first author, and it extends Hagino's categorical data types to a dependently typed setting. By basing the type theory on concepts from category theory we maintain the duality between inductive and coinductive types, and it allows us to describe, for example, the function space as a coinductive type.

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

zbMATH Keywords

dependent typesfibrationsinductive typescoinductive types

Mathematics Subject Classification ID

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

Cited In (12)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Syntax for Higher Inductive-Inductive Types
• Type theory in type theory using quotient inductive types
• Title not available (Why is that?)
• Undecidability of equality for codata types
• On generically stable types in dependent theories
• Computer Science Logic
• Dual Calculus with Inductive and Coinductive Types
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635888)