Program extraction applied to monadic parsing
- Submitting institution
-
Swansea University / Prifysgol Abertawe
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 25075
- Type
- D - Journal article
- DOI
-
10.1093/logcom/exv078
- Title of journal
- Journal of Logic and Computation
- Article number
- -
- First page
- 487
- Volume
- 29
- Issue
- 4
- ISSN
- 0955-792X
- Open access status
- Out of scope for open access requirements
- Month of publication
- December
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Program extraction from formal proofs is a powerful verification method. This is the first paper that applies program extraction to obtain correct and terminating programs in Natural Language Processing. By extracting both primitive parsers and parser combinators, it is ensured that also all complex parsers (built from these) are correct. The strength of the method is its modular style; this is difficult to achieve with other verification techniques. Two case studies, carried out in the interactive theorem prover Minlog, demonstrate that this technique not only works in theory, but is also applicable in the real world.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -