1 citations · 1 across the 3 of their papers we have counts for
6 papers · 1 filter
A Classical Linear -Calculus based on Contraposition
Pablo Barenbaum, Eduardo Bonelli, Leopoldo Lerena
We present a novel linear -calculus for Classical Multiplicative Exponential Linear Logic (\MELL) along the lines of the propositions-as-types paradigm. Starting from the standa…
Strong normalization through idempotent intersection types: a new syntactical approach
Pablo Barenbaum, Simona Ronchi Della Rocca, Cristian Sottile
It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems r…
Sharing and Linear Logic with Restricted Access (Extended Version)
Pablo Barenbaum, Eduardo Bonelli
The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechan…
Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended Version)
Pablo Barenbaum, Teodoro Freund
The lambda-PRK-calculus is a typed lambda-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical pro…
A Constructive Logic with Classical Proofs and Refutations (Extended Version)
Pablo Barenbaum, Teodoro Freund
We study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or…
Factoring Derivation Spaces via Intersection Types (Extended Version)
Pablo Barenbaum, Gonzalo Ciruelos
In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the la…