8 citations · 13 across the 6 of their papers we have counts for
4 papers · 1 filter
How to avoid the commuting conversions of IPC
José Espírito Santo, Gilda Ferreira
Since the observation in 2006 that it is possible to embed IPC into the atomic polymorphic lambda-calculus (a predicative fragment of system F with universal instantiations restric…
Typability and Type Inference in Atomic Polymorphism
M. Clarence Protin, Gilda Ferreira
It is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitati…
On Various Negative Translations
Gilda Ferreira, Paulo Oliva
Several proof translations of classical mathematics into intuitionistic mathematics have been proposed in the literature over the past century. These are normally referred to as ne…
Functional Interpretations of Intuitionistic Linear Logic
Gilda Ferreira, Paulo Oliva
We present three different functional interpretations of intuitionistic linear logic ILL and show how these correspond to well-known functional interpretations of intuitionistic lo…