Dependent Types for Mathematical Optimization, Ryan Orendorff

Note: We are now on the THIRD floor (#300) of the same building.

---

Ryan Orendorff:

Mathematical optimization is a subfield of mathematics that focuses on selecting the best element from a set of elements, often in the form of finding the element that minimizes the value of a chosen function. The algorithms developed in this field of mathematics are used to train machine learning algorithms, develop self driving cars, build safe buildings with minimal materials, and improve battery efficiency, to name only a few applications. Much of the mechanical operation of these algorithms is performed by repeated calls to linear algebra packages which, while highly tuned over many decades, provide no form of compile time guarantee that the given algorithm is correct.

In this talk, we will discuss writing numerical optimization algorithms using dependent types as a form of compile time check on the correctness of the algorithm. Dependent types allow the programmer to assert that the dimensions used in the linear algebra are correct at compile time. We will discuss the advantages of the dependently typed algorithms, as well as additional methods in which to ensure they are correct.

We will discuss a novel method of reconstructing medical images from raw data using numerical optimization. Through this example, we will explore both dependently typed linear algebra as well as functional approaches to linear algebra through matrix-free methods.

Talk repo: https://github.com/ryanorendorff/lc-2019-dependently-typed-convex-optimization

---

The building is right across the street from the Sunnyvale Caltrain station. The Target office is located on the THIRD floor. (New location!)

We will have someone in the lobby to let you in until about 6:20. After, 6:20, please leave a comment here or text 650-741-8406 and we can send someone to let you in.

Please note that there is free 3hr street and garage available parking near the building. However, you can NOT park where there are gates and/or ticket machines controlling access to the garages.