Computing

The author possesses high engineering skill in compiler technology (C++), and decent engineering skill in formalization with a proof assisant (Coq).