### 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 language | English |
---|---|

Title of host publication | Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, Proceedings |

Editors | Rosalie Iemhoff, Michael Moortgat, Ruy de Queiroz |

Publisher | Springer |

Pages | 264-281 |

Number of pages | 18 |

ISBN (Print) | 9783662595329 |

DOIs | |

Publication status | Published - 1 Jan 2019 |

Event | 26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019 - Utrecht Duration: 2 Jul 2019 → 5 Jul 2019 |

### Publication series

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

Conference | 26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019 |
---|---|

Country | Netherlands |

City | Utrecht |

Period | 2/07/19 → 5/07/19 |

### Fingerprint

### Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*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

}

*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.

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 -