No Cover Image

Journal article 356 views

Program extraction applied to monadic parsing / Ulrich Berger; Alison Jones; Monika Seisenberger

Journal of Logic and Computation, Start page: exv078

Swansea University Author: Berger, Ulrich

Full text not available from this repository: check for access using links below.

Check full text

DOI (Published version): 10.1093/logcom/exv078

Abstract

This paper 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 pa...

Full description

Published in: Journal of Logic and Computation
ISSN: 0955-792X 1465-363X
Published: 2015
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa31316
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: This paper 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 (1) a small arithmetic calculator and (2) a non-deterministic natural language parser. The work is being carried out in the interactive proof system Minlog.
Keywords: program extraction, verification, monads, parsing algorithms, natural language processing, termination, left recursion
College: College of Science
Start Page: exv078