Correctness of translations of programming languages: an algebraic approach. - F. Lockwood Morris (1972)

Advice on Structuring Compilers and Proving Them Correct. - F. Lockwood Morris (POPL, 1973)

A Metalanguage for Interactive Proof in LCF. - Michael J. C. Gordon; Robin Milner; F. Lockwood Morris; Malcolm C. Newey; Christopher P. Wadsworth (POPL, 1978)

A Time- and Space-Efficient Garbage Compaction Algorithm. - F. Lockwood Morris (Commun. ACM, 1978)

Computing Cyclic List Structures. - F. Lockwood Morris; J. Schwarz (LISP Conference, 1980)

Another Compacting Garbage Collector. - F. Lockwood Morris (Inf. Process. Lett., 1982)

An Early Program Proof by Alan Turing. - F. Lockwood Morris; Cliff B. Jones (IEEE Ann. Hist. Comput., 1984)

Domains for Logic Programming. - Ivan Filippenko; F. Lockwood Morris (Theor. Comput. Sci., 1992)

The Next 700 Formal Language Descriptions. - F. Lockwood Morris (LISP Symb. Comput., 1993)

A Generalization of the Trie Data Structure. - Richard H. Connelly; F. Lockwood Morris (Math. Struct. Comput. Sci., 1995)

A few exercises in theorem processing. - F. Lockwood Morris (Theor. Comput. Sci., 2007)