JavaScript is disabled for your browser. Some features of this site may not work without it.

## Computational Type Theory

#####
**PERMANENT LINK(S)**

#####
**Metadata**

Show full item record
#####
**Author**

Constable, Robert L.

#####
**Abstract**

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.

#####
**Date Issued**

2008-10-15#####
**Subject**

Computational; Type Theory

#####
**Type**

technical report