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

Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
Pages (from-to)4:1-4:46
JournalLogical Methods in Computer Science
Issue number2
Publication statusPublished - 22 Apr 2022

Bibliographical note

Publisher Copyright:
© G. Guerrieri, L. Pellissier, and L. Tortora de Falco.


  • Taylor expansion
  • linear logic
  • natural transformation
  • proof-structure
  • pullback

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Gluing resource proof-structures: inhabitation and inverting the Taylor expansion'. Together they form a unique fingerprint.

Cite this