Bar-Hillel Theorem Mechanization in Coq

Sergey Bozhko, Leyla Khatbullina, Semyon Grigorev

Результат исследований: Публикации в книгах, отчётах, сборниках, трудах конференцийстатья в сборнике материалов конференциинаучнаярецензирование

Аннотация

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.

Язык оригиналаанглийский
Название основной публикацииLogic, Language, Information, and Computation
Подзаголовок основной публикации26th International Workshop, Proceedings
РедакторыRosalie Iemhoff, Michael Moortgat, Ruy de Queiroz
Место публикацииBerlin, Heidelberg
ИздательSpringer Nature
Страницы264-281
ISBN (печатное издание)9783662595329
DOI
СостояниеОпубликовано - 2019
Событие26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019 - Utrecht, Голландия
Продолжительность: 2 июл 20195 июл 2019

Серия публикаций

НазваниеLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Том11541 LNCS
ISSN (печатное издание)0302-9743
ISSN (электронное издание)1611-3349

конференция

конференция26th International Workshop on Logic, Language, Information and Communication, WoLLIC 2019
СтранаГолландия
ГородUtrecht
Период2/07/195/07/19

Предметные области Scopus

  • Теоретические компьютерные науки
  • Компьютерные науки (все)

Fingerprint Подробные сведения о темах исследования «Bar-Hillel Theorem Mechanization in Coq». Вместе они формируют уникальный семантический отпечаток (fingerprint).

Цитировать