profile picture

Heiko Becker

PhD Student


I am writing up my PhD thesis and a draft of the final submission is available online

Latest Tweets

Here, I would have shown you my latests twitter post, but I cannot include external sources on my official website. You can find a copy of this site, with the tweet at

Language Skills
  • German: Native Speaker
  • English: Professional
  • French: Medium

Optimizing Programs with clang and LLVM

26. February 2020

When working with optimizing compilers, it is sometimes beneficial to inspect intermediate results to figure out whether an optimization has fired or not. While taking a dive into LLVM’s fast-math semantics I recently encountered a subtle quirk that may affect others as well.

Extending CakeML's floating-point support

04. September 2019

CakeML is an end-to-end verified compiler for a dialect of SML. Until recently it was not possible to write CakeML programs that used floating-point operations. While floating-point arithmetic was implemented throughout the backend of the compiler, it was not exposed on the frontend. Over the last weeks I have worked on a frontend implementation for CakeML, making floating-point arithmetic accessible to the end user.

Getting Fastmath Optimizations Right

31. July 2019

When using gcc or clang, programmers commonly use so-called “fastmath” optimizations to aggressively optimize floating-point programs. So far, these optimizations have been out of reach for verified compilers like CompCert or CakeML.

Data Protection Imprint