Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda
Valiant (1975) has developed an algorithm for recognition of context free languages. As of today, it remains the algorithm with the best asymptotic complexity for this purpose. In this paper, we present an algebraic specification, implementation, and proof of correctness of a generalisation of Valia...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2016-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1638/pdf |
| _version_ | 1797268619511463936 |
|---|---|
| author | Jean-Philippe Bernardy Patrik Jansson |
| author_facet | Jean-Philippe Bernardy Patrik Jansson |
| author_sort | Jean-Philippe Bernardy |
| collection | DOAJ |
| description | Valiant (1975) has developed an algorithm for recognition of context free
languages. As of today, it remains the algorithm with the best asymptotic
complexity for this purpose. In this paper, we present an algebraic
specification, implementation, and proof of correctness of a generalisation of
Valiant's algorithm. The generalisation can be used for recognition, parsing or
generic calculation of the transitive closure of upper triangular matrices. The
proof is certified by the Agda proof assistant. The certification is
representative of state-of-the-art methods for specification and proofs in
proof assistants based on type-theory. As such, this paper can be read as a
tutorial for the Agda system. |
| first_indexed | 2024-04-25T01:35:22Z |
| format | Article |
| id | doaj.art-44a5cf95b22c4995b147920104ec09a1 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:22Z |
| publishDate | 2016-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-44a5cf95b22c4995b147920104ec09a12024-03-08T09:43:58ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742016-06-01Volume 12, Issue 210.2168/LMCS-12(2:6)20161638Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in AgdaJean-Philippe BernardyPatrik Janssonhttps://orcid.org/0000-0003-3078-1437Valiant (1975) has developed an algorithm for recognition of context free languages. As of today, it remains the algorithm with the best asymptotic complexity for this purpose. In this paper, we present an algebraic specification, implementation, and proof of correctness of a generalisation of Valiant's algorithm. The generalisation can be used for recognition, parsing or generic calculation of the transitive closure of upper triangular matrices. The proof is certified by the Agda proof assistant. The certification is representative of state-of-the-art methods for specification and proofs in proof assistants based on type-theory. As such, this paper can be read as a tutorial for the Agda system.https://lmcs.episciences.org/1638/pdfcomputer science - logic in computer sciencef.4.1f.4.2 |
| spellingShingle | Jean-Philippe Bernardy Patrik Jansson Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda Logical Methods in Computer Science computer science - logic in computer science f.4.1 f.4.2 |
| title | Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda |
| title_full | Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda |
| title_fullStr | Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda |
| title_full_unstemmed | Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda |
| title_short | Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda |
| title_sort | certified context free parsing a formalisation of valiant s algorithm in agda |
| topic | computer science - logic in computer science f.4.1 f.4.2 |
| url | https://lmcs.episciences.org/1638/pdf |
| work_keys_str_mv | AT jeanphilippebernardy certifiedcontextfreeparsingaformalisationofvaliantsalgorithminagda AT patrikjansson certifiedcontextfreeparsingaformalisationofvaliantsalgorithminagda |