Damien Pous - Untyping Typed Algebras and Colouring Cyclic Linear Logic

lmcs:718 - Logical Methods in Computer Science, June 20, 2012, Volume 8, Issue 2 - https://doi.org/10.2168/LMCS-8(2:13)2012
Untyping Typed Algebras and Colouring Cyclic Linear LogicArticle

Authors: Damien Pous ORCID

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.

Comment: 21p

https://doi.org/10.2168/LMCS-8(2:13)2012
Source: arXiv.org:1205.3612
Volume: Volume 8, Issue 2
Secondary volumes: Selected Papers of the 24th International Workshop on Computer Science Logic and the 19th Annual Conference of the EACSL (CSL 2010)
Published on: June 20, 2012
Imported on: January 11, 2011
Keywords: Computer Science - Logic in Computer Science, F.4.1, F.4.3
Licence: arXiv.org - Non-exclusive license to distribute
Funding:
    Source : OpenAIRE Graph
  • Funder: French National Research Agency (ANR); Code: ANR-07-BLAN-0324
  • Formal Verification of Distributed Components; Funder: French National Research Agency (ANR); Code: ANR-10-BLAN-0305

1 Document citing this article

Share and export

Consultation statistics

This page has been seen 3193 times.
This article's PDF has been downloaded 634 times.