Home Index Table of Contents

VarDef

  • Definition of Variables

Definitions

  • Abstract Syntax
    • Types
    • Terms and Values
  • Basic Characteristics
  • Type Assigment and Subtyping

OperationProperties

  • Properties of Operations

StructuralProperties

  • Structural Properties of Full D<:

Misc

  • Miscellaneous Definitions
    • Definition of Well-formedness of Contexts
    • Definition of Structural Measures

OpeSub

  • OPE<:

Stareat

  • Definitions Related to Stare-at Subtyping
    • Definition of Revealing
    • Definition of Upcast
    • Definition of Downcast
    • Definition of Stare-at Subtyping
    • Termination of Stare-at Subtyping

Step

  • Definitions Related to Step Subtyping
    • Definition of Exposure
    • Definition of Upcast
    • Definition of Downcast
    • Definition of Step Subtyping
    • An Alternative Definition of Exposure
    • A Formalization of Termination of Step Subtyping
    • Proofs of Step Subtyping Being Algorithmic

Kernel

  • Definition and Properties of Kernel D<:
    • Lack of Transitivity
    • Soundness and Completeness of Step Subtyping w.r.t. Kernel D<:

StrongKernel

  • Definition and Properties of Strong Kernel D<:
    • Strong Kernel D<: Subsuming Kernel D<:
    • Soundness and Completeness of Stare-at Subtyping w.r.t. Strong Kernel D<:
Generated by coqdoc and improved with CoqdocJS