15 DEZEMBRO / SEXTA FEIRA / 06:23
FCUP PT 
 EN
 
 
APRESENTAÇÃO
PESSOAS
ENSINO
INVESTIGAÇÃO
BIBLIOTECA
NOTÍCIAS
CONTACTOS

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}@ncc.up.pt

Simão Melo de Sousa

LIACC, Universidade da Beira Interior
Rua Marquês d'Ávila e Bolama, 6201-001 Covilhã, Portugal
E-mail: desousa@di.ubi.pt

April 2009

Abstract

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.


FCUP 2017