Please use this identifier to cite or link to this item: https://hdl.handle.net/10216/92883
Author(s): José Bacelar Almeida
Nelma Moreira
David Pereira
Simão Melo de Sousa
Title: Partial Derivative Automata Formalized in Coq.
Issue Date: 2010
Abstract: 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.
Subject: Ciência de computadores, Ciências da computação e da informação
Computer science, Computer and information sciences
Scientific areas: Ciências exactas e naturais::Ciências da computação e da informação
Natural sciences::Computer and information sciences
URI: https://repositorio-aberto.up.pt/handle/10216/92883
Source: Implementation and Application of Automata, 17th International Conference (CIAA 2012)
Document Type: Artigo em Livro de Atas de Conferência Internacional
Rights: restrictedAccess
Appears in Collections:FCUP - Artigo em Livro de Atas de Conferência Internacional

Files in This Item:
File Description SizeFormat 
48600.pdf
  Restricted Access
Artigo181.77 kBAdobe PDF    Request a copy from the Author(s)


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.