---
_id: '13120'
abstract:
- lang: eng
  text: 'We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant.
    We defined basic notions of rewrite rules and of words derived by a grammar, and
    used grammars to show closure of the class of type-0 languages under four operations:
    union, reversal, concatenation, and the Kleene star. The literature mostly focuses
    on Turing machine arguments, which are possibly more difficult to formalize. For
    the Kleene star, we could not follow the literature and came up with our own grammar-based
    construction.'
acknowledgement: "Jasmin Blanchette: This research has received funding from the Netherlands
  Organization\r\nfor Scientific Research (NWO) under the Vidi program (project No.
  016.Vidi.189.037, Lean Forward).\r\n__\r\nWe thank Vladimir Kolmogorov for making
  this collaboration possible. We\r\nthank Václav Končický for discussing ideas about
  the Kleene star construction. We thank Patrick Johnson, Floris van Doorn, and Damiano
  Testa for their small yet very valuable contributions to our code. We thank Eric
  Wieser for simplifying one of our proofs. We thank Mark Summerfield for suggesting
  textual improvements. We thank the anonymous reviewers for very helpful comments.
  Finally, we thank the Lean community for helping us with various technical issues
  and answering many questions. "
alternative_title:
- LIPIcs
article_number: '15'
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
  full_name: Dvorak, Martin
  id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
  last_name: Dvorak
  orcid: 0000-0001-5293-214X
- first_name: Jasmin
  full_name: Blanchette, Jasmin
  last_name: Blanchette
citation:
  ama: 'Dvorak M, Blanchette J. Closure properties of general grammars - formally
    verified. In: <i>14th International Conference on Interactive Theorem Proving</i>.
    Vol 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">10.4230/LIPIcs.ITP.2023.15</a>'
  apa: 'Dvorak, M., &#38; Blanchette, J. (2023). Closure properties of general grammars
    - formally verified. In <i>14th International Conference on Interactive Theorem
    Proving</i> (Vol. 268). Bialystok, Poland: Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik. <a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">https://doi.org/10.4230/LIPIcs.ITP.2023.15</a>'
  chicago: Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars
    - Formally Verified.” In <i>14th International Conference on Interactive Theorem
    Proving</i>, Vol. 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
    <a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">https://doi.org/10.4230/LIPIcs.ITP.2023.15</a>.
  ieee: M. Dvorak and J. Blanchette, “Closure properties of general grammars - formally
    verified,” in <i>14th International Conference on Interactive Theorem Proving</i>,
    Bialystok, Poland, 2023, vol. 268.
  ista: 'Dvorak M, Blanchette J. 2023. Closure properties of general grammars - formally
    verified. 14th International Conference on Interactive Theorem Proving. ITP: International
    Conference on Interactive Theorem Proving, LIPIcs, vol. 268, 15.'
  mla: Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars
    - Formally Verified.” <i>14th International Conference on Interactive Theorem
    Proving</i>, vol. 268, 15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2023, doi:<a href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">10.4230/LIPIcs.ITP.2023.15</a>.
  short: M. Dvorak, J. Blanchette, in:, 14th International Conference on Interactive
    Theorem Proving, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
conference:
  end_date: 2023-08-04
  location: Bialystok, Poland
  name: 'ITP: International Conference on Interactive Theorem Proving'
  start_date: 2023-07-31
date_created: 2023-06-05T07:29:05Z
date_published: 2023-07-27T00:00:00Z
date_updated: 2023-09-25T11:04:29Z
day: '27'
ddc:
- '000'
department:
- _id: GradSch
- _id: VlKo
doi: 10.4230/LIPIcs.ITP.2023.15
external_id:
  arxiv:
  - '2302.06420'
file:
- access_level: open_access
  checksum: 773a0197f05b67feaa6cb1e17ec3642d
  content_type: application/pdf
  creator: dernst
  date_created: 2023-08-07T11:55:43Z
  date_updated: 2023-08-07T11:55:43Z
  file_id: '13982'
  file_name: 2023_LIPIcS_Dvorak.pdf
  file_size: 715976
  relation: main_file
  success: 1
file_date_updated: 2023-08-07T11:55:43Z
has_accepted_license: '1'
intvolume: '       268'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
publication: 14th International Conference on Interactive Theorem Proving
publication_identifier:
  eissn:
  - 1868-8969
  isbn:
  - '9783959772846'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
  link:
  - relation: software
    url: https://github.com/madvorak/grammars/tree/publish
scopus_import: '1'
status: public
title: Closure properties of general grammars - formally verified
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 268
year: '2023'
...