axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Axiom musings...


From: Tim Daly
Subject: Axiom musings...
Date: 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
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



reply via email to

[Prev in Thread] Current Thread [Next in Thread]