Reference. Certified Normalization of Context-Free Grammars

Denis Firsov, Tarmo Uustalu · CPP · 2015 · parsing · PDF · DOI · pldb
Every context-free grammar can be transformed into an equivalent one in the Chomsky normal form by a sequence of four transformations. In this work on formalization of language theory, we prove formally in the Agda dependently typed programming language that each of these transformations is correct in the sense of making progress toward normality and preserving the language of the given grammar. Also, we show that the right sequence of these transformations leads to a grammar in the Chomsky normal form (since each next transformation preserves the normality properties established by the previous ones) that accepts the same language as the given grammar. As we work in a constructive setting, soundness and completeness proofs are functions converting between parse trees in the normalized and original grammars.

Cite
Cite as @firsovCertifiedNormalizationContextFree2015 (helia, typst) · \cite{firsovCertifiedNormalizationContextFree2015} (LaTeX)
BibTeX
bibtex · 16 lines
@inproceedings{firsovCertifiedNormalizationContextFree2015,
 title = {Certified {Normalization} of {Context}-{Free} {Grammars}},
 author = {Firsov, Denis and Uustalu, Tarmo},
 year = {2015},
 isbn = {978-1-4503-3296-5},
 doi = {10.1145/2676724.2693177},
 url = {https://dl.acm.org/doi/10.1145/2676724.2693177},
 urldate = {2024-05-13},
 booktitle = {Proceedings of the 2015 {Conference} on {Certified} {Programs} and {Proofs}},
 pages = {167--174},
 publisher = {ACM},
 address = {Mumbai India},
 month = {January},
 language = {en},
 abstract = {Every context-free grammar can be transformed into an equivalent one in the Chomsky normal form by a sequence of four transformations. In this work on formalization of language theory, we prove formally in the Agda dependently typed programming language that each of these transformations is correct in the sense of making progress toward normality and preserving the language of the given grammar. Also, we show that the right sequence of these transformations leads to a grammar in the Chomsky normal form (since each next transformation preserves the normality properties established by the previous ones) that accepts the same language as the given grammar. As we work in a constructive setting, soundness and completeness proofs are functions converting between parse trees in the normalized and original grammars.}
}
hayagriva YAML (typst)
yaml · 21 lines
firsovCertifiedNormalizationContextFree2015:
  type: article
  title: Certified {Normalization} of {Context}-{Free} {Grammars}
  author:
  - Firsov, Denis
  - Uustalu, Tarmo
  date: 2015-01
  page-range: 167-174
  url:
    value: https://dl.acm.org/doi/10.1145/2676724.2693177
    date: 2024-05-13
  serial-number:
    doi: 10.1145/2676724.2693177
    isbn: 978-1-4503-3296-5
  abstract: Every context-free grammar can be transformed into an equivalent one in the Chomsky normal form by a sequence of four transformations. In this work on formalization of language theory, we prove formally in the Agda dependently typed programming language that each of these transformations is correct in the sense of making progress toward normality and preserving the language of the given grammar. Also, we show that the right sequence of these transformations leads to a grammar in the Chomsky normal form (since each next transformation preserves the normality properties established by the previous ones) that accepts the same language as the given grammar. As we work in a constructive setting, soundness and completeness proofs are functions converting between parse trees in the normalized and original grammars.
  parent:
    type: proceedings
    title: Proceedings of the 2015 {Conference} on {Certified} {Programs} and {Proofs}
    publisher:
      name: ACM
      location: Mumbai India
Download: firsovCertifiedNormalizationContextFree2015.bib · firsovCertifiedNormalizationContextFree2015.yml
Cited by (1)

CoStar: A verified ALL(*) parser lasserCoStarVerifiedALL2021PLDI · 2021
Parsers are security-critical components of many software systems, and verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited in their expressiveness, termination properties, or performance characteristics. They are only compatible with a restricted class of grammars, they are not guaranteed to terminate on all inputs, or they are not designed to be performant on grammars for real-world programming languages and data formats. In this work, we present CoStar, a verified parser that addresses these limitations. The parser is implemented with the Coq Proof Assistant and is based on the ALL(*) parsing algorithm. CoStar is sound and complete for all non-left-recursive grammars; it produces a correct parse tree for its input whenever such a tree exists, and it correctly detects ambiguous inputs. CoStar also provides strong termination guarantees; it terminates without error on all inputs when applied to a non-left-recursive grammar. Finally, CoStar achieves linear-time performance on a range of unambiguous grammars for commonly used languages and data formats.
PDF · DOI · pldb
Cites 11 works (2 here)
With notes (2)

Validating LR(1) Parsers jourdanValidatingLRParsers2012Programming Languages and Systems · 2012
An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.
PDF · DOI · pldb

Total parser combinators danielssonTotalParserCombinators2010ICFP · 2010

A monadic parser combinator library which guarantees termination of parsing, while still allowing many forms of left recursion, is described. The library’s interface is similar to those of many other parser combinator libraries, with two important differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using dependent types and a combination of induction and coinduction; and the other is that the parser type is unusually informative.

The library comes with a formal semantics, using which it is proved that the parser combinators are as expressive as possible. The implementation is supported by a machine-checked correctness proof.

PDF · DOI · pldb
External (9)
firsovCertifiedNormalizationContextFree2015 reference entries/refs/firsovCertifiedNormalizationContextFree2015/firsovCertifiedNormalizationContextFree2015.hel