Technical Report: DCC-2009-03

On the Mechanization of Kleene Algebra in Coq

Nelma Moreira, David Pereira

DCC-FC-LIACC, Universidade do Porto
R. do Campo Alegre 1021/1055 , 4169-007 Porto, Portugal
Phone: +351 220402919 , Fax: 351 22 402 950
E-mail: {nam,dpereira}

Simão Melo de Sousa

LIACC, Universidade da Beira Interior
Rua Marquês d'Ávila e Bolama, 6201-001 Covilhã, Portugal

April 2009


Kleene algebra (KA) is an algebraic system that captures properties of several important structures arising in Computer Science like automata and formal languages, among others. In this paper we present a formalization of regular languages as a KA in the COQ theorem prover. In particular, we describe the implementation of an algorithm for deciding regular expressions equivalence based on the notion of derivative. We envision the usage of (an extension of) our formalization as the formal system in which we can encode and prove proof obligations for the mechanization and automation of the process of formal software verification, in the context of the Proof Carrying Code paradigm.