8 citations · 36 across the 24 of their papers we have counts for
13 papers · 1 filter
On the Herbrand Functional Interpretation
Paulo Oliva, Chuangjie Xu
We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication…
Negative Translations for Affine and Lukasiewicz Logic
Rob Arthan, Paulo Oliva
We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in affine logic the translation schem…
Studying Algebraic Structures using Prover9 and Mace4
Rob Arthan, Paulo Oliva
In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator i…
A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic
Rob Arthan, Paulo Oliva
In this paper we introduce a term calculus which adds to the affine -calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a…
Spector bar recursion over finite partial functions
Paulo Oliva, Thomas Powell
We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions…
The Herbrand Functional Interpretation of the Double Negation Shift
Martin Escardo, Paulo Oliva
This paper considers a generalisation of selection functions over an arbitrary strong monad , as functionals of type . It is assumed throughout that…