- 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.