README Index Table of Contents

Definitions
  • Abstract Syntax
  • Opening
  • Free variables
  • Typing Rules
    • Term typing G ⊢ t: T
    • Single-definition typing G ⊢ d: D
    • Multiple-definition typing G ⊢ ds :: T
    • Subtyping G ⊢ T <: U
  • Well-typed stacks
  • Infrastructure
    • Mutual Induction Principles
    • Tactics

Binding
  • Substitution Definitions
  • Opening Lemmas
  • Variable Substitution Lemmas

RecordAndInertTypes
  • Record Types
    • Lemmas About Records and Record Types
  • Inert types

PreciseTyping
  • Precise Typing
    • Precise typing for values
  • Precise Flow
    • Precise Flow Lemmas

TightTyping
  • Tight typing G |-# t: T

Subenvironments
  • Subenvironments G1 ⪯ G2

Weakening
  • Weakening Lemma

Narrowing
  • Narrowing Lemma

InvertibleTyping
    • Invertible typing
    • Invertible typing of variables G ⊢## x: T
    • Invertible typing for values G ⊢##v v: T
    • Invertible to Precise Typing |-## to |-!
    • Invertible Subtyping Closure
    • Tight-to-Invertible Lemma for Variables |-# to |-##
  • Invertible Value Typing
    • Invertible Subtyping Closure
    • Tight-to-Invertible Lemma for Values |-# to |-##

GeneralToTight
  • Sel-<: Premise
  • Sel-<: Replacement
  • General to Tight ⊢ to ⊢#

Substitution
  • Substitution Lemma
  • Renaming

CanonicalForms
  • Simple Implications of Typing
  • Functions under Inert Contexts
  • Objects under Inert Contexts
  • Well-typedness
  • Canonical Forms for Functions
  • Canonical Forms for Objects

OperationalSemantics
  • Stack-Based Operational Semantics
    • Normal forms

Safety
  • Preservation
    • Preservation Theorem
  • Progress
    • Progress Theorem
Generated by coqdoc and improved with CoqdocJS