Kleene algebra, from automata algorithms to proof assistants

Prelegent(ci)

Damien Pous

Afiliacja

ENS Lyon

Termin

27 kwietnia 2016 14:15

Pokój

p. 5870

Seminarium

Seminarium „Teoria automatów”

---

Kleene algebra are the algebraic counterpart to finite automata on finite words. First I will describe two recent algorithms for finite automata: one exploiting bisimulations up to congruence to tame non-determinism, and one exploiting binary decision diagrams to handle large alphabets. Then I will show how such algorithms can be used to provide powerful automation tools in a proof assistant like Coq, in particular in for program certification.

---