A Proof of Virtual Types

• Matching Integer Comparisons
• Some Properties of Well-foundation
• Useful Properties of Basic Datatypes
• Definition of Syntax
• Definition of Subclassing
• Definition of Substitutions
• Definitions about De Bruijn's Indices
• Definition of Type Ordering
• Definition of Path Typing, Subtyping, Term Typing
• Definition of Semantics
• Miscellaneous properties
• Proofs about Type Ordering
• Proofs about Subclassing
• Proofs about Admissibility of Transitivity for Subtyping
• Proof of the Progress Property
• Proofs about De Bruijn's Indices
• Proofs about Substitution for the Current Instance
• Proofs about Substitution for Parameters
• Proofs about Substitution for a Local Variable
• Proof of the Subject Reduction Property
• Proof of Type Safety