Berger, Ulrich; Jones, Alison; Seisenberger, Monika Program extraction applied to monadic parsing. (English) Zbl 1452.68045 J. Log. Comput. 29, No. 4, 487-518 (2019). 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.) Keywords:program extraction; verification; monads; parsing algorithms; natural language processing; termination; left recursion; Minlog Software:Minlog PDFBibTeX XMLCite \textit{U. Berger} et al., J. Log. Comput. 29, No. 4, 487--518 (2019; Zbl 1452.68045) Full Text: DOI Link