Deciding Kleene Algebras in Coq

Details Deciding Kleene Algebras in Coq Deciding Kleene Algebras in Coq

2011-05-20

arxiv.org/abs/1105.4537v3

LMCS 8 (1:16) 2012

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-8(1:16)2012

We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations instantaneously and properly scales to larger expressions. The decision procedure is proved correct and complete: correctness is established w.r.t. any model by formalising Kozen's initiality theorem; a counter-example is returned when the given equation does not hold. The correctness proof is challenging: it involves both a precise analysis of the underlying automata algorithms and a lot of algebraic reasoning. In particular, we have to formalise the theory of matrices over a Kleene algebra. We build on the recent addition of firstorder typeclasses in Coq in order to work efficiently with the involved algebraic structures.

Affiliated with

Also associated with

No associations

Rating

Deciding Kleene Algebras in Coq does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Deciding Kleene Algebras in Coq, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Deciding Kleene Algebras in Coq will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-650394