Network protocols typically communicate via a structured binary format, relying on binary encoders and parsers to bridge the gap between these formats and the in-memory representations used by clients. Implementing parsers for such protocols, however, is a tedious and error-prone process, often involving tricky bit manipulations. The purpose of this project is to build a library for synthesizing binary encoders and parsers from mathematical specifications, allowing users to derive an implementation along with machine-checked proofs, guaranteeing its correctness. The library will extend Fiat, a deductive synthesis framework in the Coq proof assistant and is an important step towards our larger goal of automatically synthesizing internet servers from their published specifications.

I have UROPed with Prof. Chlipala last year, and that led to my interest in interactive theorem proving and functional languages. They are fun to learn.