[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Tue, 26 Nov 2019 03:56:26 -0500
Jason Gross and Adam Chlipala ("Parsing Parses") developed
a dependently typed general parser for context free grammar
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.
- Axiom musings...,
Tim Daly <=