Abstract datatypes for real numbers in type theory

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationRewriting and Typed Lambda Calculi
Subtitle of host publicationJoint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
EditorsGilles Dowek
PublisherSpringer
Pages208-223
Number of pages16
Volume8560 LNCS
ISBN (Electronic)9783319089188
ISBN (Print)9783319089171
DOIs
Publication statusPublished - 2014
Event25th 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 201417 Jul 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8560 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference25th 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/TerritoryAustria
CityVienna
Period14/07/1417/07/14

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint

Dive into the research topics of 'Abstract datatypes for real numbers in type theory'. Together they form a unique fingerprint.

Cite this