40 citations · 142 across the 19 of their papers we have counts for
4 papers · 1 filter
Innocent strategies as presheaves and interactive equivalences for CCS (expanded version)
Tom Hirschowitz, Damien Pous
Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner's CCS. We construct a category E of 'plays', and a subcategory V…
Innocent strategies as presheaves and interactive equivalences for CCS
Tom Hirschowitz, Damien Pous
Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner's CCS. We construct a category E of plays, and a subcategory V o…
Tactics for Reasoning modulo AC in Coq
Thomas Braibant, Damien Pous
We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensi…
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 a…