I am writing up my PhD thesis and a draft of the final submission is available online
Super excited that as of yesterday CakeML can optimize floating-point programs with accuracy proofs: https://t.co/XR50aSSAEN The code is the implementation for our @ECOOPconf paper "Verified Compilation and Optimization of Floating-Point Programs in CakeML"
I am a software engineer at itemis . Before that I did my PhD at MPI-SWS in the group for Automated Verification and Approximation lead by Eva Darulova . During my PhD I have worked on verified compilation and optimization of floating-point programs, and the ergonomics of interactive theorem provers.