Standard
Bar-Hillel Theorem Mechanization in Coq. / Bozhko, Sergey ; Khatbullina, Leyla; Grigorev, Semyon .
Logic, Language, Information, and Computation : 26th International Workshop, Proceedings. ed. / Rosalie Iemhoff; Michael Moortgat; Ruy de Queiroz. Berlin, Heidelberg : Springer Nature, 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: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Harvard
Bozhko, S, Khatbullina, L
& Grigorev, S 2019,
Bar-Hillel Theorem Mechanization in Coq. in R Iemhoff, M Moortgat & R de Queiroz (eds),
Logic, Language, Information, and Computation : 26th International Workshop, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11541 LNCS, Springer Nature, Berlin, Heidelberg, pp. 264-281, 26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019, Utrecht, Netherlands,
2/07/19.
https://doi.org/10.1007/978-3-662-59533-6_17
APA
Bozhko, S., Khatbullina, L.
, & Grigorev, S. (2019).
Bar-Hillel Theorem Mechanization in Coq. In R. Iemhoff, M. Moortgat, & R. de Queiroz (Eds.),
Logic, Language, Information, and Computation : 26th International Workshop, 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 Nature.
https://doi.org/10.1007/978-3-662-59533-6_17
Vancouver
Bozhko S, Khatbullina L
, Grigorev S.
Bar-Hillel Theorem Mechanization in Coq. In Iemhoff R, Moortgat M, de Queiroz R, editors, Logic, Language, Information, and Computation : 26th International Workshop, Proceedings. Berlin, Heidelberg: Springer Nature. 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
Author
Bozhko, Sergey ; Khatbullina, Leyla
; Grigorev, Semyon . /
Bar-Hillel Theorem Mechanization in Coq. Logic, Language, Information, and Computation : 26th International Workshop, Proceedings. editor / Rosalie Iemhoff ; Michael Moortgat ; Ruy de Queiroz. Berlin, Heidelberg : Springer Nature, 2019. pp. 264-281 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
BibTeX
@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",
}
RIS
TY - GEN
T1 - Bar-Hillel Theorem Mechanization in Coq
AU - Bozhko, Sergey
AU - Khatbullina, Leyla
AU - Grigorev, Semyon
N1 - 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
PY - 2019
Y1 - 2019
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
A2 - Iemhoff, Rosalie
A2 - Moortgat, Michael
A2 - de Queiroz, Ruy
PB - Springer Nature
CY - Berlin, Heidelberg
T2 - 26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019
Y2 - 2 July 2019 through 5 July 2019
ER -
