Please use this identifier to cite or link to this item:
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
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 
  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.