Please use this identifier to cite or link to this item:
http://repositorio.inesctec.pt/handle/123456789/4753
Title: | On the Formalization of Some Results of Context-Free Language Theory |
Authors: | Midena Ramos,MVM de Queiroz,RJGB Moreira,N José Bacelar Almeida |
Issue Date: | 2016 |
Abstract: | This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free 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. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formalization of the Pumping Lemma for context-free languages. |
URI: | http://repositorio.inesctec.pt/handle/123456789/4753 http://dx.doi.org/10.1007/978-3-662-52921-8_21 |
metadata.dc.type: | conferenceObject Publication |
Appears in Collections: | HASLab - Articles in International Conferences |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
P-00K-Q6M.pdf | 258.5 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.