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
Secondary volumes: Selected Papers of the 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
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)

1 Document citing this article

Share and export

Consultation statistics

This page has been seen 2602 times.
This article's PDF has been downloaded 1536 times.