Hubie Chen

CS 789 THEORY SEMINAR [home]

Speaker:  Hubie Chen
Affiliation: Computer Science, Cornell University
Date: Monday, April 28, 2003
Title: A Coalgebraic Approach to Kleene Algebra with Tests

Abstract:

Kleene Algebra with Tests is an extension of Kleene Algebra, the algebra of regular expressions, which can be used to reason about

programs. We develop a coalgebraic theory of Kleene Algebra with Tests, along the lines of the coalgebraic theory of regular

expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene Algebra with Tests does not

lend itself to a coalgebraic theory, we define a new interpretation of Kleene Algebra with Tests expressions and a corresponding

automata-theoretic presentation -- along with a type system for these notions. One outcome of the theory is a coinductive proof principle,

that can be used to establish equivalence of our Kleene Algebra with Tests expressions.  This talk will not presuppose knowledge of coalgebra.

--