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.


Source : oai:arXiv.org:1205.3612
DOI : 10.2168/LMCS-8(2:13)2012
Volume: Volume 8, Issue 2
Published on: June 20, 2012
Submitted on: June 25, 2015
Keywords: Computer Science - Logic in Computer Science,F.4.1, F.4.3


Share

Browsing statistics

This page has been seen 11 times.
This article's PDF has been downloaded 5 times.