# * Computational Type Theory -- Extended Version *

## by Robert L. Constable

2008

Computational type theory: Scholarpedia, 4(2):7618

Computational type theory provides answers to questions such as: What is a
type? What is a natural number? How do we compute with types? How are types
related to sets? Can types be elements of types? How are data types for numbers,
lists, trees, graphs, etc. related to the corresponding notions in mathematics?
What is a real number? Are the integers a subtype of the reals? Can we form the
type of all possible data types? Do paradoxes arise in formulating a theory of
types as they do in formulating a theory of sets, such as the circular idea of
the set of all sets or the idea of all sets that do not contain themselves as
members? Is there a type of all types? What is the underlying logic of type
theory? Why isn?t it the same logic in which standard set theories are
axiomatized? What is the origin of the notion of a type? What distinguishes
computational type theory from other type theories? In computational type
theory, is there a type of all computable functions from the integers to the
integers? If so, is it the same as the set of Turing computable functions from
integers to integers? Is there a type of computable functions from any type to
any type? Is there a type of the partial computable functions from a type to a
type? Are there computable functions whose values are types? Do the notations of
an implemented computational type theory include programs in the usual sense?
What does it mean that type theory is a foundational theory for both mathematics
and computer science? There have been controversies about the foundations of
mathematics, does computational type theory resolve any of them, do these
controversies impact a foundation for computing theory? This article answers
some of these questions and points to literature answering all of them.

**bibTex ref: con08B**

cite link