×

Program extraction applied to monadic parsing. (English) Zbl 1452.68045

Summary: This article outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using modified realizability, we extract formally verified and terminating programs from formal proofs. By extracting both primitive parsers and parser combinators, it is ensured that all complex parsers built from these are also correct, complete and terminating for any input. We demonstrate the viability of our approach by means of two case studies: we extract (i) a small arithmetic calculator and (ii) a non-deterministic natural language parser. The work is being carried out in the interactive proof system Minlog.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68N18 Functional programming and lambda calculus
68T50 Natural language processing
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

Minlog
PDFBibTeX XMLCite
Full Text: DOI Link