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
    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
    • Formal Verification of Distributed Components; Funder: French National Research Agency (ANR); Code: ANR-10-BLAN-0305
    • Formal Verification of Distributed Components; Funder: French National Research Agency (ANR); Code: ANR-07-BLAN-0324

    1 Document citing this article

    Share and export

    Consultation statistics

    This page has been seen 3032 times.
    This article's PDF has been downloaded 589 times.