English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Open

Presents the pdf analysis as premium feature

PDF Analysis

Insights

Presents the summarisation as premium feature

Summarisation

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

We give a new characterization of elementary and deterministic polynomialtime computation in linear logic through the proofs-as-programs correspondence.Girard's seminal results, concerning elementary and light linear logic, achievethis characterization by enforcing a stratification principle on proofs, usingthe notion of depth in proof nets. Here, we propose a more general form ofstratification, based on inducing levels in proof nets by means of indexes,which allows us to extend Girard's systems while keeping the same complexityproperties. In particular, it turns out that Girard's systems can be recoveredby forcing depth and level to coincide. A consequence of the higher flexibilityof levels with respect to depth is the absence of boxes for handling theparagraph modality. We use this fact to propose a variant of our polytimesystem in which the paragraph modality is only allowed on atoms, and which maythus serve as a basis for developing lambda-calculus type assignment systemswith more efficient typing algorithms than existing ones.

Linear Logic by Levels and Bounded Time Complexity