@conference {DBLP:conf/wia/AlmeidaMPS10,
	title = {Partial Derivative Automata Formalized in Coq},
	booktitle = {15th International Conference on Implementation and Application of Automata - CIAA - Revised Selected Papers },
	year = {2010},
	month = {August},
	pages = {59-68},
	address = {Winnipeg, MB, Canada},
	abstract = {<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>
},
	url = {http://dx.doi.org/10.1007/978-3-642-18098-9_7},
	attachments = {https://haslab.uminho.pt/sites/default/files/jba/files/10ciaa.pdf},
	author = {Jos{\'e} Bacelar Almeida and Nelma Moreira and David Pereira and Sim{\~a}o Melo de Sousa}
}