Abstract datatypes for real numbers in type theory

Martín Hötzel Escardó; Alex Simpson

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

Abstract datatypes for real numbers in type theory

Martín Hötzel Escardó, Alex Simpson

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

1 Citation (Scopus)

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
Editors	Gilles Dowek
Publisher	Springer
Pages	208-223
Number of pages	16
Volume	8560 LNCS
ISBN (Electronic)	9783319089188
ISBN (Print)	9783319089171
DOIs	https://doi.org/10.1007/978-3-319-08918-8-15
Publication status	Published - 2014
Event	25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: 14 Jul 2014 → 17 Jul 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8560 LNCS
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Conference

Conference	25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
Country/Territory	Austria
City	Vienna
Period	14/07/14 → 17/07/14

ASJC Scopus subject areas

General Computer Science
Theoretical Computer Science

Access to Document

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

Cite this

Escardó, M. H., & Simpson, A. (2014). Abstract datatypes for real numbers in type theory. In G. Dowek (Ed.), 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 LNCS, pp. 208-223). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8560 LNCS). Springer. https://doi.org/10.1007/978-3-319-08918-8-15

Escardó, Martín Hötzel ; Simpson, Alex. / Abstract datatypes for real numbers in type theory. 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. editor / Gilles Dowek. Vol. 8560 LNCS Springer, 2014. pp. 208-223 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{051846913e374aa3910db1ee67b0cd34,

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'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 Alex Simpson",

year = "2014",

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

language = "English",

isbn = "9783319089171",

volume = "8560 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "208--223",

editor = "Dowek, {Gilles }",

booktitle = "Rewriting and Typed Lambda Calculi",

note = "25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 14-07-2014 Through 17-07-2014",

}

Escardó, MH & Simpson, A 2014, Abstract datatypes for real numbers in type theory. in G Dowek (ed.), 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 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8560 LNCS, Springer, pp. 208-223, 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 14/07/14. https://doi.org/10.1007/978-3-319-08918-8-15

Abstract datatypes for real numbers in type theory. / Escardó, Martín Hötzel; Simpson, Alex.
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. ed. / Gilles Dowek. Vol. 8560 LNCS Springer, 2014. p. 208-223 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8560 LNCS).

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, Alex

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.

UR - http://www.scopus.com/inward/record.url?scp=84904748198&partnerID=8YFLogxK

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

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

M3 - Conference contribution

SN - 9783319089171

VL - 8560 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 208

EP - 223

BT - Rewriting and Typed Lambda Calculi

A2 - Dowek, Gilles

PB - Springer

T2 - 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014

Y2 - 14 July 2014 through 17 July 2014

ER -

Escardó MH, Simpson A. Abstract datatypes for real numbers in type theory. In Dowek G, editor, 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 LNCS. Springer. 2014. p. 208-223. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-08918-8-15

Abstract datatypes for real numbers in type theory

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this