5 results
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 […]
Published on June 20, 2012
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 […]
Published on March 2, 2012
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 […]
Published on September 17, 2021
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 […]
Published on May 16, 2024
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 […]
Published on July 3, 2024