CCM Colloquium: Joseph Tassarotti (NYU)

Wednesday Nov 1, 2023, 10:00 AM → 11:00 AM America/New_York

3rd Floor Classroom/3-Flatiron Institute (162 5th Avenue)

Speaker: Joseph Tassarotti (NYU)

 

Title: Verified Density Compilation for a Probabilistic Programming Language

Abstract: Compilers are complex pieces of software that are often difficult to test and debug. Moreover, compiler bugs are particularly serious because they can generate bugs in the executables the compiler produces. In recent years, researchers have applied formal verification techniques to prove the correctness of compilers, showing that executables generated by the compiler have the same behavior as the corresponding source programs. With this approach, a developer constructs a mathematical proof of the compiler's correctness using a tool called a proof assistant, which checks that each step of the proof is valid. This approach has most famously been applied in the case of CompCert, a formally verified compiler for the C programming language.

This talk describes ProbCompCert, a project with the goal of building a verified compiler for a subset of the Stan probabilistic programming language. Compilers for probabilistic programming languages like Stan apply transformations that are quite different from those performed by compilers for traditional languages. Thus, new techniques are needed to formally verify the correctness of such compilers. In this talk, I will describe the methods we have developed to verify transformations in a part of the compiler known as density compilation.

 

If you would like to attend, please email crampersad@flatironinstitute.org.