Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic

Damien Pous (1)

1 SARDES - System architecture for reflective distributed computing environments

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 the typed settings. Some of these theorems are obtained via a detour through fragments of cyclic linear logic, and give rise to a substantial optimisation of standard proof search algorithms.

Mots clés: kleene algebra; typed algebra; residuated lattice; cyclic linear logic; algebra; gentzen proof system; decision procedures; coq proof assistant

Domaines: Mathématique discrète [cs.DM]; Logique en informatique [cs.LO]; Catégories et ensembles [math.CT]

Damien Pous. Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic. Computer Science Logic, Aug 2010, Brno, Czech Republic. pp.484-498, ⟨10.1007/978-3-642-15205-4_37⟩. ⟨hal-00421158v4⟩