Of many of the following papers I offer electronically only an abstract, either because no digital copies exist, or because they appear in current publications whose copyright I have no wish to infringe. I have offprints on paper of almost all, however, and will be happy to mail copies to those who may request them. Last updated: 7/19/07.
The arrangement is reverse chronological order within each of the three areas "HOL-related", "Mathematics", and "Computer Science". ( HOL is a theorem proving system for higher-order logic.)
HOL-related:
Some Utility Tactics for HOL (2001)
Author: F. L. Morris
Status: unpublished
description (14 pp.); ML source (8 pp.); signature (2 pp.) (also linked to from "Research Interests" sub-page)
Mathematics:
Notes on G. Viennot's "Une Forme Geometrique de la Correspondance de Robinson-Schensted" (2001)
Translator/Annotator: F. L. Morris
Status: partial translation and notes for a seminar, not intended for publication, of the paper of G. Viennot in Combinatoire et Representation du Groupe Symmetrique, D. Foata ed., Springer-Verlag Lecture Notes in Mathematics 579 (1977) pp 29-58.
complete text (11 pp.)
The Beatty sequence of a real and related topics (1999)
Author: F. L. Morris
Status: notes for a seminar, not intended for publication
complete text (4 pp.)
An Algebraic Proof of the Principle of Inclusion and Exclusion (1996)
Author: F. L. Morris
Status: unpublished
complete text (2 pp.)
Computer Science
A few exercises in theorem processing (2007)
Author: F. L. Morris
Status: published, Theoretical Computer Science 375, pp 335-345; available online at www.sciencedirect.com.
abstract
Some suggestions for a possible revised presentation of IspCal (2000)
Author: F. L. Morris
Status: not intended for publication; alludes to unpublished descriptions of IspCal by S. K. Chin et al., but should be supplied with references to published work, or at least with URLs.
complete text (5 pp.)
A Generalization of the Trie Data Structure (1995)
Authors: R. H. Connelly and F. L. Morris
Status: published, Mathematical Structures in Computer Science 5, pp 381-418.
abstract
Domains for Logic Programming (1992)
Authors: I. Filippenko and F. L. Morris
Status: published, Theoretical Computer Science 94, pp 63-99.
abstract
An Early Program Proof by Alan Turing (1984)
Authors: F. L. Morris and C. B. Jones
Status: published, Annals of the History of Computing 6, 2, April 1984, pp 139-143.
abstract
Playing Disjunctive Sums is Polynomial Space Complete (1981)
Author: F. L. Morris
Status: published, International Journal of Game Theory 10, 3/4, pp 195-205.
abstract
Computing Cyclic List Structures (1980)
Authors: F. L. Morris and J. S. Schwarz
Status: presented at, and appeared in Record of, the 1980 Lisp Conference, Stanford, August 1980.
abstract
A Time- and Space-Efficient Garbage Compaction Algorithm (1978)
Author: F. L. Morris
Status: published, Communications of the ACM 21, 8, August 1978, pp 662-665.
abstract
Advice on Structuring Compilers and Proving them Correct (1973)
Author: F. L. Morris
Status: presented at, and appeared in Proceedings of, the ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages, Boston, October 1973.
introductory paragraphs
The Next 700 Formal Language Descriptions (1970)
Author: F. L. Morris
Status: has circulated in typescript since 1970; published by invitation in Higher Order and Symbolic Computation (formerly Lisp and Symbolic Computation) 6, 3, pp 249-257 (1993). available in pdf