Bulletin of Symbolic Logic 25 (2):214-214 (2019)

Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different such tools are being increasingly used in order to accelerate and simplify proof checking, and the Coq proof assistant is one of the most well known and used in large-scale projects. Language and automata theory is a well-established area of mathematics, relevant to computer science foundations and information technology. In particular, context-free language theory is of fundamental importance in the analysis, design, and implementation of computer programming languages. This work describes a formalization effort, using the Coq proof assistant, of fundamental results of the classical theory of contextfree grammars and languages. These include closure properties (union, concatenation, and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules, and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. As it turns out, this is a comprehensive formalization of the classical context-free language theory in the Coq proof assistant and includes the formalization of the Pumping Lemma for context-free languages. The perspectives for the further development of this work are diverse and can be grouped in three different areas: inclusion of new devices and results, code extraction, and general enhancements of its libraries.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1017/bsl.2019.3
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 54,740
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Coping with Unconsidered Context of Formalized Knowledge.Stefan Mandl & Bernd Ludwig - 2007 - In D. C. Richardson B. Kokinov (ed.), Modeling and Using Context. Springer. pp. 342--355.
Formalization and the Objects of Logic.Georg Brun - 2008 - Erkenntnis 69 (1):1 - 30.
Objective and Cognitive Context.Carlo Penco - 1999 - In P. Brezillon & P. Bouquet (eds.), Lecture Notes in Artificial Intelligence. Springer.
Adequate Formalization.Michael Baumgartner & Timm Lampert - 2008 - Synthese 164 (1):93-115.
How to Be Really Contraction Free.Greg Restall - 1993 - Studia Logica 52 (3):381 - 391.
Squares of Regular Languages.Gerhard Lischke - 2005 - Mathematical Logic Quarterly 51 (3):299.
Context and Content: From Language to Thought.Francois Recanati - 2011 - Contemporary Foreign Languages Studies:1-14.


Added to PP index

Total views
8 ( #930,452 of 2,386,875 )

Recent downloads (6 months)
2 ( #366,616 of 2,386,875 )

How can I increase my downloads?


My notes