Axiom musings...

Tim Daly <[email protected]> Tue, 26 Nov 2019 03:56:26 -0500

Newsgroups	gmane.comp.mathematics.axiom.devel
Message-ID	<CAJn5L=+FGXs0XSYpAfk3SeoRhK-D4mZxWUojfmpXvp_Ny2E3MQ@mail.gmail.com>

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