Gilda Ferreira

foto netI am an Assistant Professor in the Departamento de Ciencias e Tecnologia - Universidade Aberta (Portugal). I am member of Centro de Matematica, Aplicacoes Fundamentais e Investigacao Operacional CMAFcIO (FCUL, Universidade de Lisboa, Portugal) integrated in the Logic Group and colaborator at Large-Scale Informatics Systems Laboratory LaSIGE (FCUL, Universidade de Lisboa, Portugal).

I did my undergraduate degree in Mathematics in Portugal at Faculdade de Ciencias da Universidade de Lisboa FCUL. I have a Masters and a PhD in Mathematical Logic from the same University, supervised by Professor Fernando Ferreira. I worked 3 years with a post-doctoral grant in the Theory Group of the Department of Computer Science, Queen Mary University of London (QMUL), supervised by Professor Paulo Oliva; 4 years at CMAFcIO supervised by Fernando Ferreira and 3 years at LaSIGE supervised by Vasco Vasconcelos and Jose Espirito Santo.


Departamento de Matematica, Faculdade de Ciencias da Universidade de Lisboa

Office 6.2.35
gmferreira <at> fc <dot> ul <dot> pt


Research interests

-         Mathematical Logic

-         Proof Theory

-         Classical, Intuitionistic and Linear Logic

-         Realizability and Functional Interpretations

-         Bounded Arithmetic and Computational Complexity


Peer-reviewed articles


-     Typability and Type Inference in Atomic Polymorphism (with Clarence Protin), accepted for publication in Logical Methods in Computer Science (2022), 23 pages.


-     The Russell-Prawitz embedding and the atomization of universal instantiation (with Jose Espirito Santo), Logic Journal of The IGPL, 29(5):823-858 (2021). Doi:


-     A refined interpretation of intuitionistic logic by means of atomic polymorphism (with Jose Espirito Santo), Studia Logica, 108:477-507 (2020). Doi:


-     The computational content of atomic polymorphism* (with Vasco T. Vasconcelos), Logic Journal of the IGPL, 27(5):625-638 (2019). Doi:


-     Atomic polymorphism and the existence property. Annals of Pure and Applied Logic, 169(12):1303-1316 (2018). Doi:


-     A herbrandized functional interpretation of classical first-order logic (with Fernando Ferreira). Archive for Mathematical Logic, 56:523-539 (2017). Doi:

-     Analysis in weak systems (with Antonio M. Fernandes and Fernando Ferreira). Logic and Computation: Essays in Honour of Amilcar Sernadas, College Publications, 231-261 (2017).

-     Rasiowa-Harrop disjunction property. Studia Logica, 105(3):649-664 (2017). Doi:

-     Eta-conversions of IPC implemented in atomic F, Logic Journal of the IGPL, 25(2):115-130 (2017). Doi:

-     An elementary proof of strong normalization for atomic F (with Fernando Ferreira), Bulletin of the Section of Logic, 45(1):1-15 (2016). Doi:

-     Instantiation overflow (with Bruno Dinis), Reports on Mathematical Logic, 51:15-33 (2016). Doi:

-     The Faithfulness of Fat: a Proof-Theoretic Proof (with Fernando Ferreira), Studia Logica, 103(6):1303-1311 (2015). Doi:

-     The Faithfulness of Atomic Polymorphism (with Fernando Ferreira), Trends in Logic XIII, A. Indrzejczak, J. Kaczmarek, M. Zawidzki (eds.), Lodz University Press, pp. 55-64 (2014).

-     Bounded Theories for Polyspace Computability (with Ricardo Bianconi and Emmanuel Silva), Portugaliae Mathematica, 70(4):295-318 (2013). Doi:

-     Interpretability in Robinsons Q (with Fernando Ferreira). The Bulletin of Symbolic Logic, 19(3):289-317 (2013). Doi:

-     Techniques in Weak Analysis for Conservation Results (with Antonio Fernandes and Fernando Ferreira). New Studies in Weak Arithmetics, P. Cegielski, Ch. Cornaros, C. Dimitracopoulos (Eds.), CSLI Lecture Notes Number 211, pp. 115-147 (2013).

-     Atomic Polymorphism (with Fernando Ferreira). The Journal of Symbolic Logic, vol. 78, pp. 260-274 (2013). Doi:

-     On the Relation Between Various Negative Translations (with Paulo Oliva). Logic, Construction, Computation, Ontos-Verlag Mathematical Logic Series, vol. 3, pp. 227-258 (2012).

-     On Bounded Functional Interpretations (with Paulo Oliva). Annals of Pure and Applied Logic, vol. 163, n 8, pp. 1030-1049 (2012). Doi:

-     Functional Interpretations of Intuitionistic Linear Logic (with Paulo Oliva). Logical Methods in Computer Science, vol. 7 (1:9), pp. 1-22 (2011). Doi:

-     On Various Negative Translations (with Paulo Oliva), In Steffen van Bakel, Stefano Berardi, Ulrich Berger (Eds.), Poceedings of CL&C2010, Electronic Proceedings in Theoretical Computer Science, vol. 47, pp. 21 33 (2011). A full version with detailed proofs can be found here. Doi:

-     Confined Modified Realizability (with Paulo Oliva). Mathematical Logic Quarterly, vol. 56, n 1, pp. 13-28 (2010). Doi:

-     Commuting Conversions vs. the Standard Conversions of the Good Connectives (with Fernando Ferreira). Studia Logica, vol. 92, n 1, pp. 63-84 (2009). Doi:

-     The Counting Hierarchy in Binary Notation. Portugaliae Mathematica, vol. 66, n 1, pp. 81-94 (2009). Doi:

-     Functional Interpretations of Intuitionistic Linear Logic (with Paulo Oliva). In E. Gradel, R. Kahle (Eds.), Proceedings of CSL2009, Lecture Notes in Computer Science, vol. 5771, pp. 3-19, Springer (2009). DOI:

-     Harringtons Conservation Theorem Redone (with Fernando Ferreira). Archive for Mathematical Logic, vol. 47, pp. 91-100 (2008). Doi:

-     The Riemann Integral in Weak Systems of Analysis (with Fernando Ferreira). Journal of Universal Computer Science, vol. 14, n 6, pp. 908-937 (2008). Doi:

-     An interpretation of S^1_2 in ∑^b_1-NIA (with Isabel Oitavem). Portugaliae Mathematica, vol. 63, n 4, pp. 427-450 (2006).

-     Counting as Integration in Feasible Analysis (with Fernando Ferreira). Mathematical Logic Quarterly, vol. 52, n 3, pp. 315-320 (2006). Doi:

* In the acknowledgements, I forgot to write a well-deserved thanks to Jose Espirito Santo, for his help in preparing the revised version of the paper: The computational content of atomic polymorphism.


-     Sistemas de Analise Fraca para a Integracao. Ph.D. thesis (in portuguese), Universidade de Lisboa, 2006.

-     Aritmetica Computavel em Espaco Polinomial. Masters thesis (in portuguese), Universidade de Lisboa, 2001.


Expository article

-     O Conjunto de Todos os Conjuntos Nao Existe. Gazeta de Matematica, n 176, pp. 24-28 (2015).

-     Quando a Logica nao se contenta com a Verdade. Gazeta de Matematica, n 174, pp. 26-33 (2014).

Abstracts and Technical Reports

-     Atomic Polymorphism: an overview. The Bulletin of Symbolic Logic, vol. 22, n 3, pp. 379 (2016).

-     Atomic Polymorphism: an Elementary Proof of Strong Normalization. The Bulletin of Symbolic Logic, vol. 20, n 2, pp. 228 (2014).

-     Functional Interpretations of Intuitionistic Linear Logic (with Paulo Oliva). Workshop CCC09, local proceedings, Dieter Spreen editor, Universitat Siegen, pp. 22 (2009).

-     Confined Modified Realizability (with Paulo Oliva). Queen Mary - Technical Reports - RR-08-05 (2008).

-     Integration in Systems of Weak Analysis. Conference Reports, 4th International Workshop PCC05, Elbl, Kahle, Oitavem editors, Faculdade de Ciencias e Tecnologia - UNL, n 1, pp. 4-5 (2005).

-     Weak Theories of Arithmetic and the Counting Hierarchy. The Bulletin of Symbolic Logic, vol. 10, n 2, pp. 254 (2004).



Last updated: 7 July 2022