-*-text-*-

This directory contains papers produced by our research group.  Some of these
are in .dvi format, others are shar's of LaTeX source.   

Copyright notice: Those papers which have appeared or are to appear are
copyright by their respective publishers; All others are copyright by their
authors.  These materials are made available for Fair Use only.  

caap93.{dvi,shar}: 
J. Tiuryn and M. Wand, ``Type Reconstruction with Recursive
Types and Atomic Subtyping'' \tr 92-18, July, 1992; to appear in {\em {CAAP
'93: 18th Colloquium on Trees in Algebra and Programming}}, 1993.

lfp92.dvi: 
M. Wand and D. P. Oliva, ``Proving the Correctness of Storage
Representations,'' {\it Proc. 1992 ACM Conf. on Lisp and Functional
Programming,\/} 151--160.

lics90.shar:
M. Wand and Z-Y Wang,
``Conditional Lambda-Theories and the Verification of Static Properties
of Programs,'' (with Z-Y Wang), \lics{5th} (1990), 321--332. Revised version,
\tr 90-24,  to appear in {\it {Information and Computation}\/}.

mitre.shar:
D. P. Oliva and M. Wand,
``A Verified Compiler for Pure PreScheme,'' \tr 92-5, 
February, 1992.

partial-types.shar:
M. Wand and P. M. O'Keefe,
``Type Inference for Partial Types is Decidable,'' 
{\it {European Symposium on Programming '92}\/} (B. Krieg-Br\"uckner, ed.),
Springer Lecture Notes in Computer Science, Vol.~582, pp. 408--417.

proc-reps.shar:
M. Wand, 
``Correctness of Procedure Representations in Higher-Order Assembly
Language,'' {\it {Proc. MFPS '91}\/} (S. Brookes, ed.), Springer Lecture Notes
in Computer Science, Volume 598, (1992), pp. 294--311.

using-isabelle.shar:
B. Ciesielski and M. Wand,
``Using the Theorem Prover Isabelle-91 to Verify a Simple Proof of Compiler
Correctness,'' \tr 91-20, December, 1991.