Deciding Kleene Algebra Terms Equivalence in Coq
This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial d...
| Autor principal: | |
|---|---|
| Outros Autores: | , |
| Formato: | article |
| Idioma: | eng |
| Publicado em: |
2016
|
| Assuntos: | |
| Texto completo: | http://hdl.handle.net/10400.22/7356 |
| País: | Portugal |
| Oai: | oai:recipp.ipp.pt:10400.22/7356 |