No Cover Image

Journal article 357 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!
first_indexed 2016-11-26T20:29:02Z
last_indexed 2019-07-17T20:45:23Z
id cronfa31316
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-07-17T15:41:13Z</datestamp><bib-version>v2</bib-version><id>31316</id><entry>2016-11-26</entry><title>Program extraction applied to monadic parsing</title><alternativeTitle></alternativeTitle><author>Ulrich Berger</author><firstname>Ulrich</firstname><surname>Berger</surname><active>true</active><ORCID>0000-0002-7677-3582</ORCID><ethesisStudent>false</ethesisStudent><sid>61199ae25042a5e629c5398c4a40a4f5</sid><email>1033ad124f5b3817f154c6a412b415fb</email><emailaddr>CKinmB6DN60fV15NUChxf9yvqZQRJmUl2lxhnzSZE7o=</emailaddr><date>2016-11-26</date><deptcode>SCS</deptcode><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.</abstract><type>Journal article</type><journal>Journal of Logic and Computation</journal><volume/><journalNumber/><paginationStart>exv078</paginationStart><paginationEnd/><publisher></publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0955-792X</issnPrint><issnElectronic>1465-363X</issnElectronic><keywords>program extraction, verification, monads, parsing algorithms, natural language processing, termination, left recursion</keywords><publishedDay>8</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2015</publishedYear><publishedDate>2015-12-08</publishedDate><doi>10.1093/logcom/exv078</doi><url>http://logcom.oxfordjournals.org/content/early/2015/12/08/logcom.exv078.abstract</url><notes></notes><college>College of Science</college><department>Computer Science</department><CollegeCode>CSCI</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution/><researchGroup>Theoretical Computer Science</researchGroup><supervisor/><sponsorsfunders/><grantnumber/><degreelevel/><degreename>None</degreename><lastEdited>2019-07-17T15:41:13Z</lastEdited><Created>2016-11-26T17:59:13Z</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid/><order>1</order></author><author><firstname>Alison</firstname><surname>Jones</surname><orcid/><order>2</order></author><author><firstname>Monika</firstname><surname>Seisenberger</surname><orcid/><order>3</order></author></authors><documents/></rfc1807>
spelling 2019-07-17T15:41:13Z v2 31316 2016-11-26 Program extraction applied to monadic parsing Ulrich Berger Ulrich Berger true 0000-0002-7677-3582 false 61199ae25042a5e629c5398c4a40a4f5 1033ad124f5b3817f154c6a412b415fb CKinmB6DN60fV15NUChxf9yvqZQRJmUl2lxhnzSZE7o= 2016-11-26 SCS 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. Journal article Journal of Logic and Computation exv078 0955-792X 1465-363X program extraction, verification, monads, parsing algorithms, natural language processing, termination, left recursion 8 12 2015 2015-12-08 10.1093/logcom/exv078 http://logcom.oxfordjournals.org/content/early/2015/12/08/logcom.exv078.abstract College of Science Computer Science CSCI SCS Theoretical Computer Science None 2019-07-17T15:41:13Z 2016-11-26T17:59:13Z College of Science Computer Science Ulrich Berger 1 Alison Jones 2 Monika Seisenberger 3
title Program extraction applied to monadic parsing
spellingShingle Program extraction applied to monadic parsing
Berger, Ulrich
title_short Program extraction applied to monadic parsing
title_full Program extraction applied to monadic parsing
title_fullStr Program extraction applied to monadic parsing
title_full_unstemmed Program extraction applied to monadic parsing
title_sort Program extraction applied to monadic parsing
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Berger, Ulrich
author Berger, Ulrich
author2 Ulrich Berger
Alison Jones
Monika Seisenberger
format Journal article
container_title Journal of Logic and Computation
container_start_page exv078
publishDate 2015
institution Swansea University
issn 0955-792X
1465-363X
doi_str_mv 10.1093/logcom/exv078
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
url http://logcom.oxfordjournals.org/content/early/2015/12/08/logcom.exv078.abstract
document_store_str 0
active_str 1
researchgroup_str Theoretical Computer Science
description 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.
published_date 2015-12-08T04:46:55Z
_version_ 1647973096087355392
score 10.873003