Pous, Damien - Untyping Typed Algebras and Colouring Cyclic Linear Logic

lmcs:718 - Logical Methods in Computer Science, June 20, 2012, Volume 8, Issue 2
Untyping Typed Algebras and Colouring Cyclic Linear Logic

Authors: Pous, Damien

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.

DOI : 10.2168/LMCS-8(2:13)2012
Volume: Volume 8, Issue 2
Published on: June 20, 2012
Submitted on: January 11, 2011
Keywords: Computer Science - Logic in Computer Science,F.4.1, F.4.3


Consultation statistics

This page has been seen 165 times.
This article's PDF has been downloaded 183 times.