Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
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 language | English |
---|---|
Title of host publication | Logic, Language, Information, and Computation |
Subtitle of host publication | 26th International Workshop, Proceedings |
Editors | Rosalie Iemhoff, Michael Moortgat, Ruy de Queiroz |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer Nature |
Pages | 264-281 |
ISBN (Print) | 9783662595329 |
DOIs | |
State | Published - 2019 |
Event | 26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019 - Utrecht, Netherlands Duration: 2 Jul 2019 → 5 Jul 2019 |
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 11541 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference | 26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019 |
---|---|
Country/Territory | Netherlands |
City | Utrecht |
Period | 2/07/19 → 5/07/19 |
ID: 48534595