wspace-coq is an interpreter for the Whitespace programming language, written in Coq.
Inspired by WS-idr, a Whitespace interpreter in Idris made by Edwin Brady, the creator of Idris and Whitespace. If it can be done in Idris, it can be done in Coq. (See wspace/edwinb-ws-idr for an updated fork.)
This pulls from the Software Foundations book series, especially from LF/Imp and the small-step stack machine in PLF/Smallstep.