We propose an abstract datatype for a closed interval of real numbers to type theory, providing a representation-independent approach to programming with real numbers. The abstract datatype requires only function types and a natural numbers type for its formulation, and so can be added to any type theory that extends Gödel's System T. Our main result establishes that programming with the abstract datatype is equivalent in power to programming intensionally with representations of real numbers. We also consider representing arbitrary real numbers using a mantissa-exponent representation in which the mantissa is taken from the abstract interval. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Escardó, M. H., & Simpson, A. (2014). Abstract datatypes for real numbers in type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 208–223). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_15
Mendeley helps you to discover research relevant for your work.