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/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In a previous paper (of which this is a prosecution) we investigated theextraction of proof-theoretic properties of natural deduction derivations fromtheir impredicative translation into System F. Our key idea was to introduce anextended equational theory for System F codifying at a syntactic level someproperties found in parametric models. In a recent series of papers a differentapproach to extract proof-theoretic properties of natural deduction derivationswas proposed by defining predicative variants of the usual translation,embedding intuitionistic propositional logic into the atomic fragment of SystemF. In this paper we show that this approach finds a general explanation withinour equational study of second-order natural deduction, and a clear semanticjustification provided by parametricity.

The naturality of natural deduction (II). Some remarks on atomic polymorphism