Partial derivative automata formalized in Coq

• Autor(es): Almeida, José Bacelar ; Moreira, Nelma ; Pereira, David ; Sousa, Simão Melo de
• Data: 2011
• Identificador Persistente: http://hdl.handle.net/1822/13097
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Kleene algebra; Partial derivative automata; Coq
• Tipo de Documento: Documento de conferência
• Idioma: Inglês

Descrição

In this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. This proof is part of a for- malization of Kleene algebra and regular languages in Coq towards their usage in program certification.