• Verified Software Toolchain: A program logic for C and it's verified compiler.
    Verifiable C, a program logic for the C language, is proven sound with respect to the operational semantics of CompCert C. The compiler and optimizers are written and verified in Coq.
  • Cito: C-like language with a verified compiler.
    A verified compiler from the language Cito to Bedrock. Cito is a language with full support for expressions, control flow, mutable memory and function calls (for functions written in Cito, Bedrock or compiled from another source). 
  • Augmented Reality Restoration: Non-invasive color restoration of faded paintings using light from a digital projector. 
    We recreated the original color appearance of five faded paintings by illuminating them with a digital projector. We use a camera-projector system controlled by a computer. By comparison with a target image a corrective color image is calculated and projected onto the original paintings showing the original appearance of the paintings. 
  • Improved lens toy: An improved simple online optical lab.
    I added some functionality to the open source lens toy. Allowing for accurately setting the elements properties and saving setups.