Towards Specifying Symbolic Computation Jacques Carette and William M. Farmer 2019 Abstract Many interesting and useful symbolic computation algorithms manipulate mathematical expressions in mathematically meaningful ways. Although these algorithms are commonplace in computer algebra systems, they can be surprisingly difficult to specify in a formal logic since they involve an interplay of syntax and semantics. In this paper we discuss several examples of syntax-based mathematical algorithms, and we show how to specify them in a formal logic with undefinedness, quotation, and evaluation. Keywords Symbolic computation, computer algebra systems, reasoning about syntax, undefinedness, quotation and evaluation.