2 citations · 6 across the 13 of their papers we have counts for
12 papers · 1 filter
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…
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…
Hybrid Intersection Types for PCF (Extended Version)
Pablo Barenbaum, Delia Kesner, Mariana Milicich
Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then…
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,…
A Diamond Machine For Strong Evaluation
Beniamino Accattoli, Pablo Barenbaum
Abstract machines for strong evaluation of the -calculus enter into arguments and have a set of transitions for backtracking out of an evaluated argument. We study a new abstrac…
Two Decreasing Measures for Simply Typed Lambda-Terms (Extended Version)
Pablo Barenbaum, Cristian Sottile
This paper defines two decreasing measures for terms of the simply typed lambda-calculus, called the W-measure and the Tm-measure. A decreasing measure is a function that maps each…
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…
Superdevelopments for Weak Reduction
Eduardo Bonelli, Pablo Barenbaum
We study superdevelopments in the weak lambda calculus of Cagman and Hindley, a confluent variant of the standard weak lambda calculus in which reduction below lambdas is forbidden…