%0 Conference Paper
%B 15th International Conference on Implementation and Application of Automata - CIAA - Revised Selected Papers
%D 2010
%T Partial Derivative Automata Formalized in Coq
%A José Bacelar Almeida
%A Nelma Moreira
%A David Pereira
%A Simão Melo de Sousa
%C Winnipeg, MB, Canada
%P 59-68
%U http://dx.doi.org/10.1007/978-3-642-18098-9_7
%X <p>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.</p>
%8 August
%> https://haslab.uminho.pt/sites/default/files/jba/files/10ciaa.pdf