@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 = "Sergey Bozhko and Leyla Khatbullina and Semyon Grigorev",
note = "Bozhko S., Khatbullina L., Grigorev S. (2019) Bar-Hillel Theorem Mechanization in Coq. In: Iemhoff R., Moortgat M., de Queiroz R. (eds) Logic, Language, Information, and Computation. WoLLIC 2019. Lecture Notes in Computer Science, vol 11541. Springer, Berlin, Heidelberg; 26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019 ; Conference date: 02-07-2019 Through 05-07-2019",
year = "2019",
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 Nature",
pages = "264--281",
editor = "Rosalie Iemhoff and Michael Moortgat and {de Queiroz}, Ruy",
booktitle = "Logic, Language, Information, and Computation",
address = "Germany",
}