The first step is figuring out if it has been published in some form elsewhere. Recognize that people often put some draft version on their personal website to make the full text available, especially if they're not allowed to host the published version.
In this case inspecting the URL gives some hints*. Consider omitting the "joerg.pdf" part, and go to John Harrison's Complete publications list, which further links to this page. Both these pages can tell you that this document is a chapter in a handbook:
History of Interactive Theorem Proving
John Harrison, Josef Urban and Freek Wiedijk.
In Jörg Siekmann (ed), Handbook of the History of Logic, vol. 9: Computational Logic, Elsevier, pp. 135-214 (2014).
(The last link even provides a citation in bibtex form, but it uses the InProceedings form. I would probably use the InCollection style instead. Elsevier seem to agree.)
In MLA, book chapter references can be written
Last, First M. "Section Title." Book/Anthology. Ed. First M. Last. City: Publisher, Year Published. Page(s).
For this document, you'd have something like
Harrison, J., Urban, J., and Wiedijk, F. "History of Interactive Theorem Proving." Handbook of the History of Logic, vol. 9: Computational Logic, edited by Siekmann, J. Elsevier, 2014, 135--214.
*In cases when the URL doesn't reveal anything, consider searching for the title and authors in a search engine. This can often lead you to a more official version.