This is a simple certified expression compiler written in Coq as a homework
for the Coq & Type Theory course taught at the Radboud Universiteit Nijmegen.