8 citations · 13 across the 6 of their papers we have counts for
7 papers
On the Various Translations between Classical, Intuitionistic and Linear Logic
Gilda Ferreira, Paulo Oliva, Clarence Lewis Protin
Several different proof translations exist between classical and intuitionistic logic (negative translations), and intuitionistic and linear logic (Girard translations). Our aims i…
Herbrandized modified realizability
Gilda Ferreira, Paulo Firmino
Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitio…
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…
The Russell-Prawitz embedding and the atomization of universal instantiation
José Espírito Santo, Gilda Ferreira
Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system F_at, we study directly in sy…
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…