CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Logical Methods in Computer Science (1860-5974). Vol. 12 (2016), 2, p. 28.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: Context-Free Parsing, Valiant’s algorithm, Proof, Agda.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-08-31. Senast ändrad 2016-10-20.
CPL Pubid: 240990

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)