Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Fri 19 Jun 2020 15:00 - 15:20 at PLDI Research Papers live stream - Language Design II Chair(s): Mike Dodds

The real numbers are pervasive, both in daily life, and in mathematics.
Students spend much time studying their properties. Yet computers and
programming languages generally provide only an approximation geared
towards performance, at the expense of many of the nice properties we
were taught in high school.

Although this is entirely appropriate for many applications, particularly
those that are sensitive to arithmetic performance in the usual sense,
we argue that there are others where it is a poor choice.
If arithmetic computations and result are directly exposed to human users
who are not floating point experts, floating point approximations tend to be
viewed as bugs. For applications such as calculators,
spreadsheets, and various verification tasks, the cost of
precision sacrifices is high, and the performance benefit is often not critical.
We argue that previous attempts to provide accurate and understandable
results for such applications using the recursive reals
were great steps in the right direction, but they
do not suffice. Comparing recursive reals diverges if they are equal.
In many cases, comparison of numbers, including equal ones, is both important,
particularly in simple cases, and intractable in the general case.

We propose an API for a real number type that explicitly provides decidable
equality in the easy common cases, in which it is often unnatural not to.
We describe a surprisingly compact and simple implementation in detail.
The approach relies heavily on classical number theory
results. We demonstrate the utility of such a facility in two applications:
testing floating point functions, and to implement arithmetic in
Google's Android calculator application.

Fri 19 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

14:20 - 15:40: PLDI Research Papers - Language Design II at PLDI Research Papers live stream
Chair(s): Mike DoddsGalois, Inc.

YouTube lightning session video

pldi-2020-papers14:20 - 14:40
Gérard BerryCollège de France, France, Manuel SerranoInria, France
pldi-2020-papers14:40 - 15:00
Roshan DathathriUniversity of Texas at Austin, USA, Blagovesta KostovaEPFL, Switzerland, Olli SaarikiviMicrosoft Research, Redmond, Wei DaiMicrosoft Research, n.n., Kim LaineMicrosoft Research, Redmond, Madan MusuvathiMicrosoft Research
pldi-2020-papers15:00 - 15:20
pldi-2020-papers15:20 - 15:40
Stefan K. MullerCarnegie Mellon University, USA, Kyle SingerWashington University in St. Louis, USA, Noah GoldsteinWashington University in St. Louis, USA, Umut A. AcarCarnegie Mellon University, USA, Kunal AgrawalWashington University in St. Louis, USA, I-Ting Angelina LeeWashington University in St. Louis, USA