Jason Gross and Adam Chlipala ("Parsing Parses") developed
a dependently typed general parser for context free grammar
in Coq.They used the parser to prove its own completeness. Unfortunately Spad is not a context-free grammar. But it is an intersting thought exercise to consider an "Axiom on Coq" implementation. Tim
