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