Partial derivative automata formalized in Coq

• Author(s): Almeida, José Bacelar ; Moreira, Nelma ; Pereira, David ; Sousa, Simão Melo de
• Date: 2011
• Persistent ID: http://hdl.handle.net/1822/13097
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Kleene algebra; Partial derivative automata; Coq
• Document Type: Conference Object
• Language: English

Description

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.