Increasingly, computer software is used to manipulate continuous values, in domains such as machine learning, solid modeling, and scientific computing. At the same time, such programs are increasingly integrated within safety-critical systems. Usually, these algorithms are designed and analyzed assuming real-number arithmetic, whereas they are implemented with finite-precision arithmetic, such as floating point. Because finite-precision arithmetic suffers from rounding error and overflow, answers may be far from the ideal results that assume real arithmetic. Furthermore, programming with continuous values extends far beyond the reals and real arithmetic, involving objects such as probability distributions and shapes, and sometimes involving differentiation. Reasoning about the accuracy of programs that use finite-precision arithmetic to manipulate these objects is even more difficult.
My thesis proposes programming-language foundations for sound computation with continuous values, as well as datatypes and programs in these languages for representing and manipulating, in addition to real numbers, more complex objects such as probability distributions and shapes. Values may be computed to arbitrary precision, and equality of mathematical expressions corresponds to equivalence of programs in these languages (unlike floating point). λC is a language where types are generalized spaces and functions are (generalized) continuous maps. λS builds on λC to support differentiation, where types have differentiable structure and functions are (generalized) smooth maps.
To demonstrate that these languages can serve as programming-language foundations for sound computation with continuous values, I implemented λC and λS and built prototype libraries within them for solid modeling and probabilistic computing. These libraries give a proof of concept that the foundations are sufficiently expressive for a broad class of tasks.
Thesis Supervisor: Prof. Michael Carbin
Thesis Committee: Profs. Adam Chlipala, Armando Solar-Lezama
To attend this defense, please contact the doctoral candidate for details, sherm at mit dot edu