Search

• < Previous
• 1
• Next >

---

Deciding Kleene Algebras in Coq

Thomas Braibant ; Damien Pous.

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&nbsp;[&hellip;]

---

Untyping Typed Algebras and Colouring Cyclic Linear Logic

Damien Pous.

We prove "untyping" theorems: in some typed theories (semirings, Kleene algebras, residuated lattices, involutive residuated lattices), typed equations can be derived from the underlying untyped equations. As a consequence, the corresponding untyped decision procedures can be extended for free to&nbsp;[&hellip;]

---

Companions, Causality and Codensity

Damien Pous ; Jurriaan Rot.

In the context of abstract coinduction in complete lattices, the notion of compatible function makes it possible to introduce enhancements of the coinduction proof principle. The largest compatible function, called the companion, subsumes most enhancements and has been proved to enjoy many good&nbsp;[&hellip;]

---