Binary models generated by their tally part. - Fernando Ferreira 001 (Arch. Math. Log., 1994)

A Feasible Theory for Analysis. - Fernando Ferreira 001 (J. Symb. Log., 1994)

What are the forall Sigmab1-Consequences of T12 and T22? - Fernando Ferreira 001 (Ann. Pure Appl. Log., 1995)

On End-Extensions of Models of ¬exp. - Fernando Ferreira 001 (Math. Log. Q., 1996)

Extracting Algorithms from Intuitionistic Proofs. - Fernando Ferreira 001; António Marques (Math. Log. Q., 1998)

A Note on Finiteness in the Predicative Foundations of Arithmetic. - Fernando Ferreira 001 (J. Philos. Log., 1999)

Two General Results on Intuitionistic Bounded Theories. - Fernando Ferreira 001 (Math. Log. Q., 1999)

On the Consistency of the Δ11-CA Fragment of Frege's Grundgesetze. - Fernando Ferreira 001; Kai Frederick Wehmeier (J. Philos. Log., 2002)

Groundwork for Weak Analysis. - António Marques Fernandes; Fernando Ferreira 001 (J. Symb. Log., 2002)

Bounded functional interpretation. - Fernando Ferreira 001; Paulo Oliva (Ann. Pure Appl. Log., 2005)

A Simple Proof of Parsons' Theorem. - Fernando Ferreira 001 (Notre Dame J. Formal Log., 2005)

Amending Frege's Grundgesetze der Arithmetik. - Fernando Ferreira 001 (Synth., 2005)

Comments on Predicative Logic. - Fernando Ferreira 001 (J. Philos. Log., 2006)

Bounded modified realizability. - Fernando Ferreira 001; Ana Nunes (J. Symb. Log., 2006)

Counting as integration in feasible analysis. - Fernando Ferreira 001; Gilda Ferreira (Math. Log. Q., 2006)

Bounded functional interpretation and feasible analysis. - Fernando Ferreira 001; Paulo Oliva (Ann. Pure Appl. Log., 2007)

Harrington's conservation theorem redone. - Fernando Ferreira 001; Gilda Ferreira (Arch. Math. Log., 2008)

The Riemann Integral in Weak Systems of Analysis. - Fernando Ferreira 001; Gilda Ferreira (J. Univers. Comput. Sci., 2008)

Injecting uniformities into Peano arithmetic. - Fernando Ferreira 001 (Ann. Pure Appl. Log., 2009)

Commuting Conversions vs. the Standard Conversions of the "Good" Connectives. - Fernando Ferreira 001; Gilda Ferreira (Stud Logica, 2009)

The bounded functional interpretation of the double negation shift. - Patrícia Engrácia; Fernando Ferreira 001 (J. Symb. Log., 2010)

A Short Note on Spector's Proof of Consistency of Analysis. - Fernando Ferreira 001 (CiE, 2012)

Computability in Europe 2010. - Fernando Ferreira 001; Martin Hyland; Benedikt Löwe; Elvira Mayordomo (Ann. Pure Appl. Log., 2012)

Programs, Proofs, Processes. - Fernando Ferreira 001; Benedikt Löwe; Elvira Mayordomo (Theory Comput. Syst., 2012)

Interpretability in Robinson's Q. - Fernando Ferreira 001; Gilda Ferreira (Bull. Symb. Log., 2013)

Atomic polymorphism. - Fernando Ferreira 001; Gilda Ferreira (J. Symb. Log., 2013)

A New Computation of the σ-Ordinal of KPω. - Fernando Ferreira 001 (J. Symb. Log., 2014)

Nonstandardness and the bounded functional interpretation. - Fernando Ferreira 001; Jaime Gaspar (Ann. Pure Appl. Log., 2015)

Computability in Europe 2010. - Alessandra Carbone; Fernando Ferreira 001; Benedikt Löwe; Elvira Mayordomo (J. Log. Comput., 2015)

The Finitistic Consistency of Heck's Predicative Fregean System. - Luís Cruz-Filipe; Fernando Ferreira 001 (Notre Dame J. Formal Log., 2015)

The Faithfulness of Fat: A Proof-Theoretic Proof. - Fernando Ferreira 001; Gilda Ferreira (Stud Logica, 2015)

A herbrandized functional interpretation of classical first-order logic. - Fernando Ferreira 001; Gilda Ferreira (Arch. Math. Log., 2017)

Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic. - Bruno Dinis; Fernando Ferreira 001 (Math. Log. Q., 2017)

The FAN principle and weak König's lemma in herbrandized second-order arithmetic. - Fernando Ferreira 001 (Ann. Pure Appl. Log., 2020)

Bounds for Indexes of Nilpotency in Commutative Ring Theory: a Proof Mining Approach. - Fernando Ferreira 001 (Bull. Symb. Log., 2020)

On False Heine/Borel Compactness Principles in Proof Mining. - Fernando Ferreira 001 (CiE, 2021)

The abstract type of the real numbers. - Fernando Ferreira 001 (Arch. Math. Log., 2021)