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 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. As a consequence, we prove also semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.

Guerrieri, G., Pellissier, L., TORTORA DE FALCO, L. (2022). Gluing resource proof-structures: inhabitation and inverting the Taylor expansion. LOGICAL METHODS IN COMPUTER SCIENCE.

Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

Tortora de Falco Lorenzo
2022

Abstract

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 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. As a consequence, we prove also semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.
Guerrieri, G., Pellissier, L., TORTORA DE FALCO, L. (2022). Gluing resource proof-structures: inhabitation and inverting the Taylor expansion. LOGICAL METHODS IN COMPUTER SCIENCE.
File in questo prodotto:
File Dimensione Formato  
2022-3-18-Arxiv-LMCS-FinalVersion.pdf

accesso aperto

Descrizione: articolo principale
Tipologia: Documento in Pre-print
Licenza: DRM non definito
Dimensione 1.04 MB
Formato Adobe PDF
1.04 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11590/404460
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact