Links: Index_v Table of contents Main page

• Presentation of the formalization
  • General notice
  • Quick pointers
  • Excerpt from the manuscript
• Indexed Calculus
  • Definition
    • Terms
    • Functions
    • Reduction
    • Errors and valid terms
  • Properties
• Strong normalization of the untyped Indexed Calculus
• Semantics of the Indexed Calculus
  • Definition of types
    • Set properties
    • Sound terms
    • The closure operator
    • Pretype and types
    • Properties
  • The arrow and product operators
  • The forall operator
  • The pi operator
  • The exists operator
  • The top and bottom operators
  • Recursive types
    • The mu operator
    • The notion of k-approximation
    • The notion of well-foundness and non-expansiveness
    • Computational types are well-founded
    • Erasable types are non-expansive
  • Semantic judgment
    • Soundness of the computational typing rules
    • Soundness of erasable rules
• Lambda Calculus
  • Definition
  • Functions
  • Reduction
  • Errors and valid terms
  • Strong normalization
  • Properties about lift and subst
  • Values
• System Fcc (common part)
  • Syntax
    • Objects
    • Syntactical classes
    • Functions
  • Judgments
    • Well-foundness
    • Equality
    • Objects
• System Fcc (lambda version)
• System Fcc (indexed version)
• Soundness of the indexed version of System Fcc
  • Interpretation
    • Object interpretation
    • Semantic lifting
    • Semantic substitution
  • Soundness
    • Well-foundness
    • Semantic class
    • Equality
    • Objects
    • Terms
• Soundness of the lambda version of System Fcc
  • Sound terms
  • Term judgments equivalence
  • Soundness
• Semantics of the Lambda Calculus
  • Definition of types
    • Set properties
    • The closure operator
    • Pretype and types
    • Properties
  • The arrow and product operators
  • The forall operator
  • The pi operator
  • The exists operator
  • The top and bottom operators
  • Semantic judgment
    • Soundness of the computational typing rules
    • Soundness of erasable rules
• Strong normalization of the lambda version of System Fcc
  • Interpretation
    • Object interpretation
    • Semantic lifting
    • Semantic substitution
  • Soundness
    • Semantic class
    • Equality
    • Objects
    • Terms

Links: Index_v Table of contents Main page