PhD 2020 & MS 2016, Computer Science, Cornell University
n k o u n k o u (a) c s . c o r n e l l . e d u
I used Coq to mechanically formalize the semantics of CHP (Communicating Hardware Processes, a high-level language used to design asynchronous circuits) and build a certified CHP simulator.
I used Coq to mechanically prove that our newly developed CHP semantics used in our CHP-error-detection tool are equivalent to the commonly accepted CHP semantics.