[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
- Axiom musings...,
Tim Daly <=