Sciweavers

Share
CSL
2010
Springer

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

11 years 2 months ago
Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic
Abstract. 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.
Damien Pous
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CSL
Authors Damien Pous
Comments (0)
books