Bar Induction and Pi11-CA1. - Harvey Friedman (J. Symb. Log., 1969)

The Consistency of Classical Set Theory Relative to a Set Theory with Intuitionistic Logic. - Harvey Friedman (J. Symb. Log., 1973)

Borel Sets and Hyperdegrees. - Harvey M. Friedman (J. Symb. Log., 1973)

PCA Well-Orderings of the Line. - Harvey Friedman (J. Symb. Log., 1974)

On Existence Proofs of Hanf Numbers. - Harvey Friedman (J. Symb. Log., 1974)

One Hundred and Two Problems in Mathematical Logic. - Harvey Friedman (J. Symb. Log., 1975)

A cumulative hierarchy of predicates. - Harvey Friedman (Math. Log. Q., 1975)

Uniformly Defined Descending Sequences of Degrees. - Harvey Friedman (J. Symb. Log., 1976)

On the Derivability of Instantiation Properties. - Harvey Friedman (J. Symb. Log., 1977)

Computational Complexity of Real Functions. - Ker-I Ko; Harvey Friedman (Theor. Comput. Sci., 1982)

Set existence property for intuitionistic theories with dependent choice. - Harvey M. Friedman; Andrej Scedrov (Ann. Pure Appl. Log., 1983)

Countable algebra and set existence axioms. - Harvey M. Friedman; Stephen G. Simpson; Rick L. Smith (Ann. Pure Appl. Log., 1983)

Large sets in intuitionistic set theory. - Harvey M. Friedman; Andrej Scedrov (Ann. Pure Appl. Log., 1984)

On the Spectra of Universal Relational Sentences - Harvey Friedman (Inf. Control., 1984)

Addendum to "countable algebra and set existence axioms". - Harvey M. Friedman; Stephen G. Simpson; Rick L. Smith (Ann. Pure Appl. Log., 1985)

Epistemic and intuitionistic formal systems. - Robert C. Flagg; Harvey M. Friedman (Ann. Pure Appl. Log., 1986)

Intuitionistically provable recursive well-orderings. - Harvey M. Friedman; Andre Scedrov (Ann. Pure Appl. Log., 1986)

Maximality in modal logic. - Robert C. Flagg; Harvey M. Friedman (Ann. Pure Appl. Log., 1987)

Lindenbaum algebras of intuitionistic theories and free categories. - Peter J. Freyd; Harvey Friedman; Andre Scedrov (Ann. Pure Appl. Log., 1987)

An axiomatic approach to self-referential truth. - Harvey M. Friedman; Michael Sheard (Ann. Pure Appl. Log., 1987)

The disjunction and existence properties for axiomatic systems of truth. - Harvey M. Friedman; Michael Sheard (Ann. Pure Appl. Log., 1988)

A Borel Reducibility Theory for Classes of Countable Structures. - Harvey Friedman; Lee J. Stanley (J. Symb. Log., 1989)

The Equivalence of the Disjunction and Existence Properties for Modal Arithmetic. - Harvey Friedman; Michael Sheard (J. Symb. Log., 1989)

Weak Comparability of Well Orderings and Reverse Mathematics. - Harvey Friedman; Jeffry L. Hirst (Ann. Pure Appl. Log., 1990)

Reverse Mathematics and Homeomorphic Embeddings. - Harvey Friedman; Jeffry L. Hirst (Ann. Pure Appl. Log., 1991)

Whither Relevant Arithmetic? - Harvey Friedman; Robert K. Meyer (J. Symb. Log., 1992)

Periodic Points and Subsystems of Second-Order Arithmetic. - Harvey Friedman; Stephen G. Simpson; Xiaokang Yu (Ann. Pure Appl. Log., 1993)

Elementary Descent Recursion and Proof Theory. - Harvey Friedman; Michael Sheard (Ann. Pure Appl. Log., 1995)

Some Decision Problems of Enormous Complexity. - Harvey Friedman (LICS, 1999)

Does mathematics need new axioms? - Solomon Feferman; Harvey M. Friedman; Penelope Maddy; John R. Steel (Bull. Symb. Log., 2000)

Subtle cardinals and linear orderings. - Harvey M. Friedman (Ann. Pure Appl. Log., 2001)

Long Finite Sequences. - Harvey M. Friedman (J. Comb. Theory A, 2001)

Primitive Independence Results. - Harvey M. Friedman (J. Math. Log., 2003)

Expansions of o-minimal structures by fast sequences. - Harvey Friedman; Chris Miller 001 (J. Symb. Log., 2005)

Combining decision procedures for the reals. - Jeremy Avigad; Harvey Friedman (Log. Methods Comput. Sci., 2006)

What is o-minimality? - Harvey M. Friedman (Ann. Pure Appl. Log., 2008)

A language for mathematical language management - Steven Kieffer; Jeremy Avigad; Harvey Friedman (CoRR, 2008)

Expansions of the real field by open sets: definability versus interpretability. - Harvey Friedman; Krzysztof Kurdyka; Chris Miller 001; Patrick Speissegger (J. Symb. Log., 2010)

Building a push-button RESOLVE verifier: Progress and challenges. - Murali Sitaraman; Bruce M. Adcock; Jeremy Avigad; Derek Bronish; Paolo Bucci; David Frazier; Harvey M. Friedman; Heather K. Harton; Wayne D. Heym; Jason Kirschenbaum; Joan Krone; Hampton Smith; et al. (Formal Aspects Comput., 2011)

Syrus: providing practice problems in discrete mathematics with instant feedback. - Diego Zaccai; Aditi Tagore; Dustin Hoffman; Jason Kirschenbaum; Zakariya Bainazarov; Harvey M. Friedman; Dennis K. Pearl; Bruce W. Weide (SIGCSE, 2014)

Perspectives on formal verification (invited talk). - Harvey M. Friedman (CPP, 2016)

This Foundationalist Looks at P = NP. - Harvey Friedman (ACM SIGSOFT Softw. Eng. Notes, 2018)