Giulio Guerrieri ; Luc Pellissier ; Lorenzo Tortora de Falco - Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

lmcs:6705 - Logical Methods in Computer Science, April 22, 2022, Volume 18, Issue 2 - https://doi.org/10.46298/lmcs-18(2:4)2022
Gluing resource proof-structures: inhabitation and inverting the Taylor expansionArticle

Authors: Giulio Guerrieri ORCID; Luc Pellissier ; Lorenzo Tortora de Falco

    A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.

    https://doi.org/10.46298/lmcs-18(2:4)2022
    Source: arXiv.org:2008.03103
    Volume: Volume 18, Issue 2
    Published on: April 22, 2022
    Accepted on: May 31, 2021
    Submitted on: August 10, 2020
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03F52, 03B47, 03B70
    Licence: Attribution 4.0 International (CC BY 4.0)

    Share and export

    Consultation statistics

    This page has been seen 2027 times.
    This article's PDF has been downloaded 1136 times.