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...

Full description

Bibliographic Details
Main Author: Pereira, David (author)
Other Authors: Moreira, Nelma (author), Sousa, Simão Patrício Melo de (author)
Format: article
Language:eng
Published: 2016
Subjects:
Proof assistants
Regular expressions
Kleene algebra with tests
Program verification
Online Access:http://hdl.handle.net/10400.22/7356
Country:Portugal
Oai:oai:recipp.ipp.pt:10400.22/7356

Internet

http://hdl.handle.net/10400.22/7356

Similar Items