Type theory based on dependent inductive and coinductive types

DOI10.1145/2933575.2934514MaRDI QIDQ4635888zbMATHOpenAlexFDO

Authors 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

dependent typesfibrationsinductive typescoinductive types

Mathematics Subject Classification ID

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

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.

Recommendations

• Dependent inductive and coinductive types are fibrational dialgebras
• Algebra and Coalgebra in Computer Science
• Inductive, coinductive, and pointed types
• scientific article; zbMATH DE number 1342222
• Dual Calculus with Inductive and Coinductive Types

Cited in

(16)

• A syntax for higher inductive-inductive types
• scientific article; zbMATH DE number 7168147 (Why is no real title available?)
• Terminal semantics for codata types in intensional Martin-Löf type theory
• Algebra and Coalgebra in Computer Science
• Inductive, coinductive, and pointed types
• Dual Calculus with Inductive and Coinductive Types
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• Type theory in type theory using quotient inductive types
• scientific article; zbMATH DE number 7649955 (Why is no real title available?)
• Quotients, inductive types, and quotient inductive types
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• Undecidability of equality for codata types
• Computer Science Logic
• scientific article; zbMATH DE number 7168146 (Why is no real title available?)
• Dependent inductive and coinductive types are fibrational dialgebras
• On generically stable types in dependent theories

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)