A Soundness Proof of Virtual Types
----------------------------------

This archive contains a formalization in Coq (Coq is a proof assistant
developed at INRIA available at http://coq.inria.fr/) of a type safety
proof for virtual types. Virtual types provide a powerful mechanism of
type abstraction in the domain of object-oriented languages. The
provided definitions and proofs follow closely the contents of Chapter
3 (and Appendix A) of my PhD thesis report entitled "Foundations for
Scala: Semantics and Proof of Virtual Types" (EPFL, Thesis No. 3556,
May 2006).

The proof has been checked with Coq version 8.0pl1 (Jul 2004).

It requires to have the CoLoR library (a Coq library on rewriting and
termination) installed, for its formalization of multisets.

For letting Coq check the proof, use the command "make".

For generating documentation (without the proofs), use the command
"make forcedoc".

Here is the structure of this archive:

- README       : the present file.
- <files>.v    : the definitions and lemmas of my proof.
- CoLoR.tar.gz : the version of the CoLoR library I used.
- Makefile     : basic makefile for checking the proof and building the
                 documentation.
- doc/         : the directory containing the generated HTML documentation
                 (See toc.html).
- thesis.ps    : my PhD thesis report (See Chapter 3 and Appendix A).

If you encounter any problem, send a mail to Vincent Cremet at
vincent.cremet@epfl.ch.

Vincent Cremet, Lausanne, August 2006.