Projects per year
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 (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 language | English |
---|---|
Journal | Logical Methods in Computer Science |
Volume | 18 |
Issue number | 2 |
DOIs | |
Publication status | Published - 22 Apr 2022 |
Projects
- 1 Active
-
Typed Lambda-Calculi with Sharing and Unsharing
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council