Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
426381 | Information and Computation | 2016 | 26 Pages |
Abstract
We prove that given two cut-free nets of linear logic, by means of their relational interpretations one can determine: 1) whether or not the net obtained by cutting the two nets is strongly normalizable, 2) (in case it is strongly normalizable) the maximum length of the reduction sequences starting from that net. As a by-product of our semantic approach, we obtain a new proof of the conservation theorem for Multiplicative Exponential Linear Logic (MELL) which does not rely on confluence; this yields an alternative proof of strong normalization for MELL.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Daniel de Carvalho, Lorenzo Tortora de Falco,