Document details

Partial Derivative Automata Formalized in Coq.

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

Date: 2010

Origin: Repositório Aberto da Universidade do Porto

Subject(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


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

Document Type Book
Language English
facebook logo  linkedin logo  twitter logo 
mendeley logo

Related documents