Detalhes do Documento

Partial Derivative Automata Formalized in Coq.

Autor(es): José Bacelar Almeida ; Nelma Moreira ; David Pereira ; Simão Melo de Sousa

Data: 2010

Origem: Repositório Aberto da Universidade do Porto

Assunto(s): Ciência de computadores, Ciências da computação e da informação; Computer science, Computer and information sciences; Ciência de computadores, Ciências da computação e da informação; Ciência de computadores, Ciências da computação e da informação; Computer science, Computer and information sciences; Computer science, Computer and information sciences


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 formalization of Kleene algebra and regular languages in Coq towards their usage in program certification.

Tipo de Documento Livro
Idioma Inglês
facebook logo  linkedin logo  twitter logo 
mendeley logo

Documentos Relacionados