Abstract Datatypes for Real Numbers in Type Theory

Martín Hötzel Escardó; Alexander Simpson

doi:10.1007/978-3-319-08918-8_15

Abstract Datatypes for Real Numbers in Type Theory

Martín Hötzel Escardó, Alexander Simpson

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Rewriting and Typed Lambda Calculi
Subtitle of host publication	Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
Publisher	Springer
Pages	208-223
Number of pages	16
Volume	8560
ISBN (Electronic)	978-3-319-08918-8
ISBN (Print)	978-3-319-08917-1
DOIs	https://doi.org/10.1007/978-3-319-08918-8_15
Publication status	Published - 2014

Access to Document

10.1007/978-3-319-08918-8_15

Escardo and Simpson 2014 Abstract DatatypesAccepted author manuscript, 347 KB

http://dx.doi.org/10.1007/978-3-319-08918-8_15

Cite this

@inproceedings{de292c1c03b7485a94ad2b29af03e909,

title = "Abstract Datatypes for Real Numbers in Type Theory",

abstract = "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{\"o}del{\textquoteright}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.",

author = "Escard{\'o}, \{Mart{\'i}n H{\"o}tzel\} and Alexander Simpson",

year = "2014",

doi = "10.1007/978-3-319-08918-8\_15",

language = "English",

isbn = "978-3-319-08917-1",

volume = "8560",

pages = "208--223",

booktitle = "Rewriting and Typed Lambda Calculi",

publisher = "Springer",

address = "United Kingdom",

}

Abstract Datatypes for Real Numbers in Type Theory. / Escardó, Martín Hötzel; Simpson, Alexander.
Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Vol. 8560 Springer, 2014. p. 208-223.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Abstract Datatypes for Real Numbers in Type Theory

AU - Escardó, Martín Hötzel

AU - Simpson, Alexander

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-08918-8_15

DO - 10.1007/978-3-319-08918-8_15

M3 - Conference contribution

SN - 978-3-319-08917-1

VL - 8560

SP - 208

EP - 223

BT - Rewriting and Typed Lambda Calculi

PB - Springer

ER -

Abstract Datatypes for Real Numbers in Type Theory

Abstract

Access to Document

Fingerprint

Cite this