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;]

---

Petri Automata

Paul Brunet ; Damien Pous.

Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras&nbsp;[&hellip;]

---

A Distribution Law for CCS and a New Congruence Result for the pi-calculus

Daniel Hirschkoff ; Damien Pous.

We give an axiomatisation of strong bisimilarity on a small fragment of CCS that does not feature the sum operator. This axiomatisation is then used to derive congruence of strong bisimilarity in the finite pi-calculus in absence of sum. To our knowledge, this is the only nontrivial subcalculus of&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;]

---

Modular coinduction up-to for higher-order languages via first-order transition systems

Jean-Marie Madiot ; Damien Pous ; Davide Sangiorgi.

The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible&nbsp;[&hellip;]

---

On Tools for Completeness of Kleene Algebra with Hypotheses

Damien Pous ; Jurriaan Rot ; Jana Wagemaker.

In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance&nbsp;[&hellip;]

---

Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines

Małgorzata Biernacka ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk ; Damien Pous ; Alan Schmitt.

We present fully abstract encodings of the call-by-name and call-by-value $\lambda$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $\lambda$-calculus side -- normal-form bisimilarity, applicative bisimilarity, and&nbsp;[&hellip;]

---

Completeness Theorems for Kleene algebra with tests and top

Damien Pous ; Jana Wagemaker.

We prove two completeness results for Kleene algebra with tests and a top element, with respect to guarded string languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an&nbsp;[&hellip;]

---