Extracting Monadic Parsers from Proofs
Authors: Ulrich Berger, Alison Jones and Monika Seisenberger
Paper Information
| Title: | Extracting Monadic Parsers from Proofs |
| Authors: | Ulrich Berger, Alison Jones and Monika Seisenberger |
| Proceedings: | PSC 2014 Abstracts |
| Editors: | Peter Schuster, Dirk Pattinson and Ana Sokolova |
| Keywords: | Minlog, Parser, Monad, Set-theory, Termination, Extraction |
| Abstract: | ABSTRACT. This talk outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using a modified realisability interpretation, we extract provably correct and terminating programs from formal proofs. If the proof system is proven to be correct, then any extracted program is guaranteed to be so. By extracting parsers, we can ensure that they are correct, complete and terminating for any input. The work is ongoing, and is being carried out in the interactive proof system Minlog. |
| Pages: | 2 |
| Talk: | Jul 18 10:45 |
| Paper: |  |