Harvey M. Friedman

ACM SIGSOFT Softw. Eng. Notes, 2018

2016

Perspectives on formal verification (invited talk).

[BibT_eX]

[DOI]

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2014

Syrus: providing practice problems in discrete mathematics with instant feedback.

[BibT_eX]

[DOI]

Proceedings of the 45th ACM Technical Symposium on Computer Science Education, 2014

2011

Building a push-button RESOLVE verifier: Progress and challenges.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2011

2010

Expansions of the real field by open sets: definability versus interpretability.

[BibT_eX]

[DOI]

J. Symb. Log., 2010

2008

A language for mathematical language management

[BibT_eX]

[DOI]

Steven Kieffer

Jeremy Avigad

CoRR, 2008

What is o-minimality?

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2008

2006

Combining decision procedures for the reals.

[BibT_eX]

[DOI]

Jeremy Avigad

Log. Methods Comput. Sci., 2006

2005

Expansions of o-minimal structures by fast sequences.

[BibT_eX]

[DOI]

Chris Miller

J. Symb. Log., 2005

2003

Primitive Independence Results.

[BibT_eX]

[DOI]

J. Math. Log., 2003

2001

Long Finite Sequences.

[BibT_eX]

[DOI]

J. Comb. Theory, Ser. A, 2001

Subtle cardinals and linear orderings.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2001

2000

Does mathematics need new axioms?

[BibT_eX]

[DOI]

Bull. Symb. Log., 2000

1999

Some Decision Problems of Enormous Complexity.

[BibT_eX]

[DOI]

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1995

Elementary Descent Recursion and Proof Theory.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1995

1993

Periodic Points and Subsystems of Second-Order Arithmetic.

[BibT_eX]

[DOI]

Stephen G. Simpson

Xiaokang Yu

Ann. Pure Appl. Log., 1993

1992

Whither Relevant Arithmetic?

[BibT_eX]

[DOI]

Robert K. Meyer

J. Symb. Log., 1992

1991

Reverse Mathematics and Homeomorphic Embeddings.

[BibT_eX]

[DOI]

Jeffry L. Hirst

Ann. Pure Appl. Log., 1991

1990

Weak Comparability of Well Orderings and Reverse Mathematics.

[BibT_eX]

[DOI]

Jeffry L. Hirst

Ann. Pure Appl. Log., 1990

1989

The Equivalence of the Disjunction and Existence Properties for Modal Arithmetic.

[BibT_eX]

[DOI]

J. Symb. Log., 1989

A Borel Reducibility Theory for Classes of Countable Structures.

[BibT_eX]

[DOI]

Lee J. Stanley

J. Symb. Log., 1989

1988

The disjunction and existence properties for axiomatic systems of truth.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1988

1987

An axiomatic approach to self-referential truth.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1987

Lindenbaum algebras of intuitionistic theories and free categories.

[BibT_eX]

[DOI]

Peter J. Freyd

Andre Scedrov

Ann. Pure Appl. Log., 1987

Maximality in modal logic.

[BibT_eX]

[DOI]

Robert C. Flagg

Ann. Pure Appl. Log., 1987

1986

Intuitionistically provable recursive well-orderings.

[BibT_eX]

[DOI]

Andre Scedrov

Ann. Pure Appl. Log., 1986

Epistemic and intuitionistic formal systems.

[BibT_eX]

[DOI]

Robert C. Flagg

Ann. Pure Appl. Log., 1986

1985

Addendum to "countable algebra and set existence axioms".

[BibT_eX]

[DOI]

Stephen G. Simpson

Rick L. Smith

Ann. Pure Appl. Log., 1985

1984

On the Spectra of Universal Relational Sentences

[BibT_eX]

[DOI]

Inf. Control., 1984

Large sets in intuitionistic set theory.

[BibT_eX]

[DOI]

Andrej Scedrov

Ann. Pure Appl. Log., 1984

1983

Countable algebra and set existence axioms.

[BibT_eX]

[DOI]

Stephen G. Simpson

Rick L. Smith

Ann. Pure Appl. Log., 1983

Set existence property for intuitionistic theories with dependent choice.

[BibT_eX]

[DOI]

Andrej Scedrov

Ann. Pure Appl. Log., 1983

1982

Computational Complexity of Real Functions.

[BibT_eX]

[DOI]

Ker-I Ko

Theor. Comput. Sci., 1982

1977

On the Derivability of Instantiation Properties.

[BibT_eX]

[DOI]

J. Symb. Log., 1977

1976

Uniformly Defined Descending Sequences of Degrees.

[BibT_eX]

[DOI]

J. Symb. Log., 1976

1975

A cumulative hierarchy of predicates.

[BibT_eX]

[DOI]

Math. Log. Q., 1975

One Hundred and Two Problems in Mathematical Logic.

[BibT_eX]

[DOI]

J. Symb. Log., 1975

1974

On Existence Proofs of Hanf Numbers.

[BibT_eX]

[DOI]

J. Symb. Log., 1974

PCA Well-Orderings of the Line.

[BibT_eX]

[DOI]

J. Symb. Log., 1974

1973

Borel Sets and Hyperdegrees.

[BibT_eX]

[DOI]

J. Symb. Log., 1973

The Consistency of Classical Set Theory Relative to a Set Theory with Intuitionistic Logic.

[BibT_eX]

[DOI]

J. Symb. Log., 1973

1969

Bar Induction and Pi11-CA1.

[BibT_eX]

[DOI]