5 papers
Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)
Pablo Barenbaum
This paper explores epistemic realizability, a form of realizability in which the property that a piece of data constitutes evidence for a logical proposition is semi-decidable. In…
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…
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 stand…
Useful Evaluation: Syntax and Semantics (Technical Report)
Pablo Barenbaum, Delia Kesner, Mariana Milicich
This work provides the first inductive definition of useful CBV evaluation. For that, we first restrict the substitution operation in the Value Substitution Calculus to be linear,…
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…