W. R. Bevier, Kit: A Study in Operating System Verification,*IEEE Transactions on
Software Engineering*, November, 1989.

An Approach to Systems Verification, W. R. Bevier, W. A. Hunt, J S. Moore and
W. D. Young, *Journal of Automated Reasoning*, November, 1989. Also appears as
CLI Technical Report 41.

W. R. Bevier, Kit and the Short Stack, *Journal of
Automated Reasoning*, November, 1989.

Toward Verified Execution Environments, W. R. Bevier, W. A. Hunt and W. D. Young,
*Proc. IEEE Symposium on Security and Privacy*, April, 1987. Reprinted in Rein
Turn (editor), *Advances in Computer System Security, Volume III*, Artech
House, Inc., 1988. Also appears as CLI Technical Report 5.

The Boyer-Moore Theorem Prover and Its Interactive Enhancement, R. S. Boyer, M. Kaufmann
and J S. Moore, *Computers and Mathematics with Applications*,
Vol 29, No. 2, pp. 27-62, 1995.

Automated Correctness Proofs of Machine Code Programs for a Commercial
Microprocessor, R. S. Boyer, Yuan Yu, in D. Kapur, editor, *Automated Deduction
-- CADE-11*, Lecture Notes in Computer Science 607, Springer-Verlag,
1992, pp. 416-430.

A Biographical Sketch of W. W. Bledsoe, R. S. Boyer, Anne Boyer, in Robert S.
Boyer, editor, *Automated Reasoning: Essays in Honor of Woody Bledsoe*.
Kluwer Academic, Dordrecht, The Netherlands, 1991, pp. 1-29.

MJRTY - A Fast Majority Vote Algorithm, R. S. Boyer, J S. Moore, in Robert S.
Boyer, editor, *Automated Reasoning: Essays in Honor of Woody Bledsoe*.
Kluwer Academic, Dordrecht, The Netherlands, 1991, pp. 105-117.

Functional Instantiation in First Order Logic, R. S. Boyer, D. Goldschlag, M.
Kaufmann, and J Moore, in V. Lifschitz (editor), *Artificial
Intelligence and Mathematical Theory of Computation: Papers in Honor
of John McCarthy*. Academic Press, 1991, pp. 7-26.

A Theorem Prover for a Computational Logic, R. S. Boyer, J S. Moore, keynote
address, *Automated Deduction -- CADE-10*, Lecture Notes in Computer
Science 449, Springer-Verlag, 1990, pp. 1-15.

The Use of a Formal Simulator to Verify a Simple Real Time Control
Program, R. S. Boyer, M. W. Green and J S. Moore. in W. H. J. Feijen, A. J.
M. van Gasteren, D. Gries, and J. Misra, editors, *Beauty is Our
Business*, Springer-Verlag, 1990, pp. 54-66.

The Efficient Implementation of Lattice Operations, R. S. Boyer, H. Ait-Kaci,
P. Lincoln, and R. Nasr. *Association for Computing Machinery
Transactions on Programming Languages and Systems*, Vol. 11, No. 1,
pp. 115-146, January 1988.

The Addition of Bounded Quantification and Partial Functions to a
Computational Logic and Its Theorem Prover, R. S. Boyer, J S. Moore, *Journal
of Automated Reasoning*, Volume 4, pp. 117-172, 1988.

Integrating Decision Procedures into Heuristic Theorem Provers: A Case
Study of Linear Arithmetic, R. S. Boyer, J S. Moore. *Machine
Intelligence 11*, Oxford University Press, 1988, pp. 83-124.

Set Theory in First Order Logic: Clauses for Goedel's Axioms, R. S. Boyer, E.
Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos, *Journal of
Automated Reasoning*, Vol. 2, No. 3., pp. 287-327, 1986.

Program Verification, R. S. Boyer, J S. Moore. *Automated Reasoning*, Vol. 1,
No. 1, 1985, pp. 17-23.

A Mechanical Proof of the Turing Completeness of PURE LISP, R. S. Boyer, J S.
Moore. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary
Mathematics, Volume 29, *Automated Theorem Proving: After 25 Years*,
American Mathematical Society, Providence, Rhode Island, 1984, pp.
132-168.

Proof-Checking, Theorem-Proving, and Program Verification, R. S. Boyer,
J S. Moore. In W. W. Bledsoe and D. W. Loveland, editors,
Contemporary Mathematics, Volume 29, *Automated Theorem Proving:
After 25 Years*, American Mathematical Society, Providence, Rhode
Island, 1984, pp. 119-132.

Proof Checking the RSA Public Key Encryption Algorithm, R. S. Boyer,
J S. Moore. *American Mathematical Monthly*, Vol. 91, No. 3, March
1984, pp. 181-189.

A Mechanical Proof of the Unsolvability of the Halting Problem, R. S. Boyer,
J S. Moore. *Journal of the Association for Computing Machinery*, Vol.
31, No. 3, July 1984, pp.441-458.

A Verification Condition Generator for FORTRAN, R. S. Boyer, J S. Moore. In
R. S. Boyer and J S. Moore, editors, *The Correctness Problem in
Computer Science*, Academic Press, London, 1981, pp. 9-101.

Metafunctions: Proving Them Correct and Using Them Efficiently as New
Proof Procedures, R. S. Boyer, J S. Moore. In R. S. Boyer and J S. Moore,
editors, *The Correctness Problem in Computer Science*, Academic Press,
London, 1981, pp. 103-184.

A Lemma Driven Automatic Theorem Prover for Recursive Function Theory,
R. S. Boyer, J S. Moore. *Proceedings of the 5th International Joint Conference
on Artificial Intelligence*, pp. 511-519, 1977.

A Fast String Searching Algorithm, R. S. Boyer, J S. Moore. *Communications of
the Association for Computing Machinery*, Vol. 20, No. 10, pp. 762-772,
1977.

Proving Theorems about LISP Functions, R. S. Boyer, J S. Moore. *Journal of
the Association for Computing Machinery*, Vol. 22, No. 1, pp. 129-144,
1975.

The Sharing of Structure in Theorem-proving Programs, R. S. Boyer, J S. Moore.
In B. Meltzer and D. Michie, editors, *Machine Intelligence, Vol. 7*,
pp. 101-116, Edinburgh University Press, 1972.

Computer Proofs of Limit Theorems, R. S. Boyer, W. W. Bledsoe and W. H.
Henneman, *Artificial Intelligence*, Vol. 3, No. 1, pp. 27-60, 1972.

R. S. Boyer, The preface to *Machine Proofs in Geometry: Automated Production of
Readable Proofs for Geometry Theorems*, Shang-Ching Chou, Xiao-Shan
Gao, and Jing-Zhong Zhang, World Scientific, 1994, pp. vii-viii.
R. S. Boyer, Response, biographical sketch, and photo on the occasion of
receipt of the 1991 AMS Current Award for Automatic Theorem Proving,
*Notices of the American Mathematical Society*, vol. 38, no. 5, pp.
407-408.

A Theorem-Prover for Recursive Functions, R. S. Boyer, J S. Moore. *Software
Engineering Notes*, Association for Computing Machinery, Vol. 5, No. 3,
pp. 26-27, 1980.

The FORTRAN Verification System, R. S. Boyer, J S. Moore. *Software
Engineering Notes*, Association for Computing Machinery, Vol. 5, No.
3, pp. 16-17, 1980.

(D. I. Good, R.L. London, W.W. Bledsoe) An Interactive Program Verification
System, *IEEE Transactions on Software Engineering*, Vol. 1,
No. 1, March 1975.

(D. I. Good, L.C. Ragland) Certification of Algorithm 386(AI), Greatest
Common Division of Integers and Multipliers, *Communications
of the ACM*, Vol. 16, No. 4, April, 1973.

(D. I. Good, R.L. London) Computer Interval Arithmetic: Definition and Proof of Correct Implication. Journal of the ACM, Vol. 17, No. 4, October, 1970.

(D. I. Good, A.R. Tripathi, W. D. Young, J.C. Browne) HAL/S/V: A
Verifiable Subset of HAL/S, in *Sigplan Notices*, March, 1981.

(D. I. Good, W. D. Young) Steelman and the Verifiability of (Preliminary)
Ada, In *Sigplan Notices*, February, 1981.

(D. I. Good, W. D. Young, A.R. Tripathi, J.C. Browne) Design of a
Verifiable Subset for HAL/S, [Technical Note] In *Journal
of Guidance and Control*, January, 1981.

(D. I. Good, D.R. Musser, R.T. Yeh) New Directions in Teaching in the
Fundamentals of Computer Science - Discrete Structures and
Computational Analysis, *SIGSCE Bulletin*, Vol. 5, ACM,
February 1973.

(D. I. Good, L.C. Ragland) Nucleus - A Language of Provable Programs,
In *Program Test Methods*, Prentice Hall, 1972.

D. I. Good, Constructing Verified and Reliable Communications Processing
Systems, *ACM Software Engineering Notes*, October, 1977.

Introduction to a Formally Defined Hardware Description Language,
W. H. Hunt, Bishop C. Brock and W. D. Young, *Theorem Provers in
Circuit Design*, IFIP, North-Holland, 1992.

The Formalization of an HDL and its use in the FM8502 Microprocessor
Fabrication, W. H. Hunt, Bishop C. Brock, *Philosophical Transactions
of the Royal Society*, Volume 339, 1992.

Report on the Formal Specification and Partial Verification of the
VIPER Microprocessor, W. H. Hunt, Bishop C. Brock, *COMPASS 1991
Proceedings*, IEEE, 1991.

An Introduction to a Simple HDL, W. H. Hunt, Bishop C. Brock,
*Formal Methods for VLSI Design*, Elsevier Science Publishers,
1990.

The Verification of a Bit-Slice ALU, W. H. Hunt, Bishop C. Brock,
*Workshop on Hardware Specification, Verification and Synthesis:
Mathematical Aspects*, Lecture Notes in Computer Science, Volume
408, Springer Verlag, 1989.

W. H. Hunt, Microprocessor Design Verification, *Journal of Automated Reasoning*,
Volume 5, 1989.

An Approach to Systems Verification, W. H. Hunt, William R. Bevier, J
Strother Moore, and W. D. Young, *Journal of Automated
Reasoning*, Volume 5, 1989.

The Boyer-Moore Theorem Prover and Its Interactive Enhancement (M. Kaufmann,
Robert S. Boyer and J Strother Moore), *Computers and Mathematics with
Applications*, Vol. 29, No. 2, pp. 27-62, 1995.

M. Kaufmann,
An Extension of the Boyer-Moore Theorem Prover to Support First-Order
Quantification, *Journal of Automated Reasoning*, Vol. 9, No. 3.,
December 1992, pp. 355-372.

Functional Instantiation in First Order Logic (M. Kaufmann, Robert S. Boyer,
David M. Goldschlag, and J Strother Moore), in: *Artificial
Intelligence and Mathematical Theory of Computation: Papers in Honor
of John McCarthy*, Academic Press, 1991, pp. 7 - 26.

M. Kaufmann, Generalization in the Presence of Free Variables: a
Mechanically-Checked Correctness Proof for One Algorithm. *Journal
of Automated Reasoning* 7(1991), pp. 109-158.

Remarks on Weak Notions of Saturation in Models of Peano Arithmetic
(M. Kaufmann, J. Schmerl). *Journal Symbolic Logic*, 52 (1987), pp. 129-148.

The Hanf Number of Stationary Logic (M. Kaufmann, S. Shelah). *Notre Dame J.
Formal Logic*, 27 (1986), pp. 111-123.

M. Kaufmann, A Note on the Hanf Number of Second-Order Logic. *Notre Dame J. Formal
Logic*, 26 (1985), 305-308.

M. Kaufmann, The Quantifier *There Exist Uncountably Many* and Some of Its Relatives.
In *Model-Theoretic Logics*, (J. Barwise and S. Feferman, editors).
Springer-Verlag, 1985, pp. 123-176.

On Random Models of Finite Power and Monadic Logic (M. Kaufmann, S. Shelah).
*Discrete Mathematics*, 54 (1985), pp. 285-293.

M. Kaufmann, On Expandability of Models of Arithmetic and Set Theory to Models of Weak
Second-Order Theories. *Fund. Math.*, CXXII (1984), pp. 57-60.

M. Kaufmann, Some Remarks on Equivalence in Infinitary and Stationary Logic. Notre
Dame J. *Formal Logic*, 25 (1984), pp. 383-389.

Saturation and Simple Extensions of Models of Peano Arithmetic (M. Kaufmann, J.
Schmerl) *Ann. Pure and Applied Logic*, 27 (1984), pp.109-136.

The Strength of Nonstandard Methods in Arithmetic (M. Kaufmann, C.W. Henson and
H.J. Keisler). *J. Symbolic Logic*, 49 (1984), pp. 1039-1058.

A Nonconservativity Result on Global Choice (M. Kaufmann, S. Shelah). *Ann. Pure
and Applied Logic*, 27 (1984), pp. 209-214.

M. Kaufmann, Mutually Generic Classes and Incompatible Expansions. *Fund. Math.*, CXXI
(1984), pp. 213-218.

Definable Ultrapowers and Ultrafilters over Admissible Ordinals (M. Kaufmann,
E. Kranakis). Zeitschr.f. Math. *Logik und Grund.*, d. Math. 30 (1984),
pp.97-118.

M. Kaufmann, Filter Logics on W. *J. Symbolic Logic*, 49 (1984), pp. 241-256.

M. Kaufmann, Blunt and Topless End Extensions of Models of Set Theory. *J Symbolic
Logic*, 48 (1983), pp. 1053-1071.

M. Kaufmann, Set Theory with a Filter Quantifier. *J. of Symbolic Logic*, 48 (1983),
pp. 263-287.

SUM-1-Well-founded Compactness (M. Kaufmann, N. Cutland). *Ann. Math Logic*, 18
(1980), pp. 271-296.

M. Kaufmann, Filter logics: Filters on W-1. *Ann. Math. Logic*, 20 (1980),
pp. 155-200.

M. Kaufmann, A New Omitting Types Theorem for L(Q). *J. Symbolic Logic*, 44 (1979),
pp. 217-231.

Stationary Logic (M. Kaufmann, J. Barwise and M. Makkai). *Ann. Math. Logic*, 13
(1978), pp. 171-224.

A Correction to *Stationary Logic* (M. Kaufmann, J. Barwise and M. Makkai). *Ann.
Math. Logic*, 20 (1981), pp. 231-232.

M. Kaufmann, A Rather Classless Model. *Proceedings Amer. Math. Soc.*, 62 (1977),
pp. 330-333.

Smith, M. K., Siebert, A., DiVito, B. and Good, D.
A verified encrypted packet interface,
*Software Engineering Notes*,
Volume 6, Number 3, July 1981.

Good, D. and Smith, M. K.
A verified distributed system,
*Software Engineering Notes*,
Volume 5, Number 3, July 1980.

J S. Moore, A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol. In

Formal Aspects of Computing, Vol 6, #1, 1994, pp. 60-91.

J S. Moore, Introduction to the OBDD Algorithm for the ATP Community. In

Journal of Automated Reasoning, Kluwer Academic Publishers, Vol 6, #1, 1994, pp. 33-45.

Functional Instantiation in First Order Logic, J S. Moore, R.S. Boyer, D.M. Goldschlag, and M. Kaufmann. In V. Lifschitz, editor,

Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, pp. 7-26.

MJRTY - A Fast Majority Vote Algorithm, J S. Moore, R.S. Boyer. In R.S. Boyer, editor,

Automated Reasoning: Essays in Honor of Woody Bledsoe, Automated Reasoning Series, Kluwer Academic Publishers, Dordrecht, The Netherlands, 1991, pp. 105-117.

The Use of a Formal Simulator to Verify a Simple Real Time Control Program,
J S. Moore, R.S. Boyer and M.W. Green, in W.H.J. Feijen, A.J.M. van Gasteren, D.
Gries, and J. Misra* editors, *

*Beauty is Our Business: A Birthday Salute to
Edsger W. Dijkstra*, Springer-Verlag Texts and Monographs in Computer Science,
1990, pp. 54-66.

Special Issue on System Verification, J S. Moore, W.R. Bevier, W. A. Hunt, and W.D.
Young. *Journal of Automated Reasoning*, Kluwer Academic Publishers, Vol 5, #4,
1989, pp. 461-492.

J S. Moore, A Mechanically Verified Language Implementation. In *Journal of Automated
Reasoning*, Kluwer Academic Publishers, Vol 5, #4, 1989, pp. 461-492.

The Addition of Bounded Quantification and Partial Functions to A
Computational Logic and Its Theorem Prover, J S. Moore, R. S. Boyer. In *Journal of
Automated Reasoning*, Kluwer Academic Publishers, Vol 4, #2, 1988, pp. 117-172.

Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study
of Linear Arithmetic, J S. Moore, R.S. Boyer. In *Machine Intelligence*, Oxford
University Press (1988)

Program Verification, J S. Moore, R.S. Boyer. *Automated Reasoning*, Vol. 1, #1, 1985,
pp. 17-23.

A Mechanical Proof of the Turing Completeness of PURE LISP, J S. Moore, R. S. Boyer.
In W. W. Bledsoe and D. W. Loveland, editors, *Contemporary Mathematics*, Volume
29, Automated Theorem Proving: After 25 Years, American Mathematical Society,
Providence, Rhode Island, 1984, pp. 133-168.

Proof-Checking, Theorem-Proving, and Program Verification, J S. Moore, R. S. Boyer.
In W. W. Bledsoe and D. W. Loveland, editors, *Contemporary Mathematics*, Volume
29, Automated Theorem Proving: After 25 Years, American Mathematical Society,
Providence, Rhode Island, 1984, pp. 119-132.

A Mechanical Proof of the Unsolvability of the Halting Problem, J S. Moore, R. S.
Boyer. *Journal of the Association for Computing Machinery*, Vol. 31, No. 3,
July 1984, pp. 441-458.

Proof Checking the RSA Public Key Encryption Algorithm, J S. Moore, R. S. Boyer.
*American Mathematical Monthly*, Vol. 91, No. 3, March 1984, pp. 181-189.

A Verification Condition Generator for FORTRAN, J S. Moore, R.S. Boyer. In R.S. Boyer
and J S. Moore, editors, *The Correctness Problem in Computer Science*, Academic
Press, London, 1981.

Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof
Procedures, J S. Moore, R.S. Boyer. In R.S. Boyer and J S. Moore, editors, *The
Correctness Problem in Computer Science*, Academic Press, London, 1981.

J S. Moore, A Mechanical Proof of the Termination of Takeuchi's Function. *Information
Processing Letters*, Vol. 9, No. 4, pp. 176-181, 1979.

A Fast String Searching Algorithm, J S. Moore, R.S. Boyer. *Communications of the
Association for Computing Machinery*, Vol. 20, No. 10, pp. 762-772, 1977.

J S. Moore, Introducing Iteration into the Pure LISP Theorem-Prover. *IEEE Transactions on
Software Engineering*, Vol. SE-1, No. 3, pp. 328-338, 1975.

Proving Theorems about LISP Functions, J S. Moore, R.S. Boyer. *Journal of the
Association for Computing Machinery*, Vol. 22, No. 1, pp.129-144, 1975.

The Sharing of Structure in Theorem-proving Programs, J S. Moore, R.S. Boyer. In
B. Meltzer and D. Michie, editors, *Machine Intelligence*, Vol. 7, pp. 101-116,
Edinburgh University Press, 1972.

Program Verification: An Approach to Reliable Hardware and Software, J S. Moore,
L. Lamport. *Transactions of the American Nuclear Society, American Nuclear
Society*, Vol. 35, pp 252-253, November, 1980.

A Theorem-Prover for Recursive Functions, J S. Moore, R.S. Boyer. *Software Engineering
Notes, Association for Computing Machinery*, Vol. 5, No. 3, pp. 26-27, 1980.

The FORTRAN Verification System, J S. Moore, R.S. Boyer. *Software Engineering Notes*,
Association for Computing Machinery, Vol. 5, No. 3, pp. 16-17, 1980.

J S. Moore, A Statement of Position. *Software Engineering Notes*, Association for Computing
Machinery, Vol. 5, No. 3, pp 23-24, 1980.

J S. Moore, Automatic Proof of the Correctness of a Binary Addition Algorithm. *
SIGART Newsletter*, Association for Computing Machinery, No. 52, pp. 13-14, 1975.

W. D. Young. Verifying a Simple Real-Time System with
Nqthm, CLI technical report 93, September, 1993. Also to appear in
Michael Hinchey and Jonathan Bowen, editors, *Applications of
Formal Methods*, Prentice-Hall Series in Computer Science, 1995.

W. D. Young. System Verification and the CLI Stack,
to appear in Jonathan Peter Bowen, editor, *Towards Verified
Systems*, Elsevier Science Publishers Series on Real-Time Safety
Critical Systems: Amsterdam, 1993.

Mathematical Methods for Digital Systems Development, W. D. Young, Donald
I. Good, in *VDM'91 Formal Software Development Methods*, S. Prehn,
W.J. Toetenel, editors, Springer-Verlag Lecture Notes in Computer
Science 552, pp. 406-430, 1991. Also appears as CLI technical report
67, August, 1991.

Machine Checked Proofs of the Design of a Fault-Tolerant Circuit,
W. D. Young, William R. Bevier, to appear in *Formal Aspects of
Computing*. Also appears as CLI technical report 62,
Computational Logic, Inc., August, 1990.

The Design and Proof of Correctness of a Fault-Tolerant Circuit,
W. D. Young, William R. Bevier, in *Dependable Computing for Critical
Applications*, J.F. Meyer and R.D. Schlichting, editors,
Springer-Verlag, Vienna, 1991, pp. 243-260. Also
appears as CLI technical report 57, August, 1990.

An Approach to Systems Verification, W. D. Young, W.R. Bevier, W. A. Hunt,
and J S. Moore, *Journal of Automated Reasoning* , Vol. 5, Number 4,
(December, 1989), pp. 411-428. Also available from Computational
Logic as CLI technical report 41.

W. D. Young, A Mechanically Verified Code Generator, *Journal of Automated
Reasoning*, Vol. 5, Number 4, (December, 1989), pp. 493-518. Also
available from Computational Logic as CLI technical report 37.

Toward Verified Execution Environments, W. D. Young, W.R. Bevier and W.A.
Hunt, *Proc. IEEE Symposium on Security and Privacy*, April, 1987.
Reprinted in Rein Turn (editor), *Advances in Computer System Security,
Volume III*, Artech House, Inc., 1988. Also available from Computational
Logic as CLI technical report 5.

Experience using Two Covert Channel Analysis Techniques on a Real
System Design, W. D. Young, J.T. Haigh, J. McHugh and R.A. Kemmerer,
*Proc. IEEE Symposium on Security and Privacy*, April, 1986, pp. 14-24.
Reprinted in *IEEE Transactions on Software Engineering*, January, 1987.

Extending the Non-Interference Version of MLS for SAT, W. D. Young, J.T.
Haigh, *Proc. IEEE Symposium on Security and Privacy*, April, 1986,
pp. 232-239. Received best paper award at the Symposium. Reprinted
in *IEEE Transactions on Software Engineering*, January, 1987.
Reprinted in Rein Turn (editor), *Advances in Computer System
Security, Volume III*, Artech House, Inc., 1988.

The Extended Access Matrix Model of Computer Security, W. D. Young, W.E.
Boebert and R.Y. Kain, *Software Engineering Notes*, (August, 1985),
vol. 10, no. 4, pp. 119-125.

Proving a Computer System Secure, W. D. Young, W.E. Boebert and R.Y. Kain,
*The Scientific Honeyweller* (July, 1985), vol. 6, no. 2, pp. 18-27.
Reprinted in *Tutorial: Computer and Network Security*, eds.
Marshall D. Abrams and Harold J. Podell, IEEE Computer Society Press,
Washington, D.C., October, 1986. Reprinted in Rein Turn (editor),
*Advances in Computer System Security, Volume III*, Artech House,
Inc., 1988.

Secure Computing: The Secure Ada Target Approach, W. D. Young, W.E. Boebert
and R.Y. Kain, *The Scientific Honeyweller* (July, 1985), vol. 6,
no. 2, pp. 1017. Reprinted in * Tutorial: Computer and Network
Security*, eds. Marshall D. Abrams and Harold J. Podell, IEEE Computer
Society Press, Washington, D.C., October, 1986. Reprinted in Rein
Turn (editor), *Advances in Computer System Security, Volume III*,
Artech House, Inc., 1988.

The Role of the Family in `There Are No Madmen Here' by Gina
Valdes, W. D. Young, Dolly J. Young, presented at Third Student Conference
on Latin America, The University of Texas at Austin, April, 1983.
Also appeared as a review in *Revista Chicano-Riquena*, vol. XIII,
no. 1 (Spring, 1985), pp. 97-99.

The New Journalism in Mexico: Two Women Writers, W. D. Young, Dolly J.
Young, *Chasqui Revista de Literatura Latinoamericana* 12:2,
Febrero/Mayo, 1983, pp. 72-80. Also presented at the Southwest
Conference on Latin American Studies, Abilene, Texas, March, 1982.

HAL/S/V: A Verifiable Subset of HAL/S, W. D. Young, A.R. Tripathi, D.I. Good,
J.C. Browne, *Sigplan Notices* (March, 1981), pp. 102-113.

Steelman and the Verifiability of (Preliminary) Ada, W. D. Young, D.I. Good,
*Sigplan Notices* (February, 1981), pp. 113-119.

Design of a Verifiable Subset for HAL/S, W. D. Young, A.R. Tripathi, D.I.
Good, J.C. Browne, Technical note in *Journal of Guidance and
Control* (January, 1981), pp. 86-87.

http://dirleton.csres.utexas.edu/staff/publications/refereed.html