Bar-Hillel Theorem Mechanization in Coq

Leyla Khatbullina

Research output

Abstract

Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verification, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theorem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.

Original languageEnglish
Title of host publicationLogic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings
EditorsRosalie Iemhoff, Michael Moortgat, Ruy de Queiroz
PublisherSpringer
Pages264-281
Number of pages18
ISBN (Print)9783662595329
DOIs
Publication statusPublished - 1 Jan 2019
Event26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019 - Utrecht
Duration: 2 Jul 20195 Jul 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11541 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019
CountryNetherlands
CityUtrecht
Period2/07/195/07/19

Fingerprint

Mechanization
Formal languages
Formal Languages
Theorem
Context free languages
Intersection
Regular Sets
Context-free Languages
Formal Verification
Justification
Correctness
Closed
Graph in graph theory

Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Khatbullina, L. (2019). Bar-Hillel Theorem Mechanization in Coq. In R. Iemhoff, M. Moortgat, & R. de Queiroz (Eds.), Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings (pp. 264-281). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11541 LNCS). Springer. https://doi.org/10.1007/978-3-662-59533-6_17
Khatbullina, Leyla. / Bar-Hillel Theorem Mechanization in Coq. Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings. editor / Rosalie Iemhoff ; Michael Moortgat ; Ruy de Queiroz. Springer, 2019. pp. 264-281 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{dc7f7fe9b1a2408dad659265abdb59d6,
title = "Bar-Hillel Theorem Mechanization in Coq",
abstract = "Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verification, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theorem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.",
keywords = "Bar-Hillel theorem, Closure, Context-free language, Coq, Formal languages, Intersection, Regular language",
author = "Leyla Khatbullina",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-662-59533-6_17",
language = "English",
isbn = "9783662595329",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "264--281",
editor = "Rosalie Iemhoff and Michael Moortgat and {de Queiroz}, Ruy",
booktitle = "Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings",
address = "Germany",

}

Khatbullina, L 2019, Bar-Hillel Theorem Mechanization in Coq. in R Iemhoff, M Moortgat & R de Queiroz (eds), Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11541 LNCS, Springer, pp. 264-281, Utrecht, 2/07/19. https://doi.org/10.1007/978-3-662-59533-6_17

Bar-Hillel Theorem Mechanization in Coq. / Khatbullina, Leyla.

Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings. ed. / Rosalie Iemhoff; Michael Moortgat; Ruy de Queiroz. Springer, 2019. p. 264-281 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11541 LNCS).

Research output

TY - GEN

T1 - Bar-Hillel Theorem Mechanization in Coq

AU - Khatbullina, Leyla

PY - 2019/1/1

Y1 - 2019/1/1

N2 - Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verification, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theorem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.

AB - Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verification, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theorem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.

KW - Bar-Hillel theorem

KW - Closure

KW - Context-free language

KW - Coq

KW - Formal languages

KW - Intersection

KW - Regular language

UR - http://www.scopus.com/inward/record.url?scp=85068615424&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-59533-6_17

DO - 10.1007/978-3-662-59533-6_17

M3 - Conference contribution

AN - SCOPUS:85068615424

SN - 9783662595329

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 264

EP - 281

BT - Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings

A2 - Iemhoff, Rosalie

A2 - Moortgat, Michael

A2 - de Queiroz, Ruy

PB - Springer

ER -

Khatbullina L. Bar-Hillel Theorem Mechanization in Coq. In Iemhoff R, Moortgat M, de Queiroz R, editors, Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings. Springer. 2019. p. 264-281. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-59533-6_17