taypsi.base

• Classes
• Lemmas
• More setoid rewriting for sets
• Notations

taypsi.tactics

• Fold over hypotheses
• General purpose tactics
  • Set solving
  • Forward reasoning
  • Hypothesis application
  • General solvers

taypsi.ln

• Atom
• Tactics for cofinite quantifiers

taypsi.semilattice

• Semi-lattice
• Theorems
• Instances
• Tactics

taypsi.prelude

taypsi.lang_taypsi.base

taypsi.lang_taypsi.syntax

• Definitions
  • Obliviousness label
  • Expressions (e, τ)
  • Global definitions (D)
  • Global context (Σ)
  • Programs (P)
• Notations for expressions
• More Definitions
  • Variable opening
  • Substitution
  • Oblivious type values (ω)
  • Oblivious values (v)
  • Values (v)
  • Local closure and well-formedness of expressions
• Notations

taypsi.lang_taypsi.semantics

• Definitions
  • OADT value typing
  • Evaluation context (ℇ)
  • Small-step relation
• Notations

taypsi.lang_taypsi.kind

• Definitions
  • Kinds (κ)
• Properties
• Notations

taypsi.lang_taypsi.typing

• Definitions
  • Typing context (Γ)
  • Parallel reduction
  • Expression equivalence
  • Typing and kinding
  • Global definitions typing
  • Program typing
  • Well-formedness of global context
• Notations

taypsi.lang_taypsi.indistinguishable

• Indistinguishability
• Notations

taypsi.lang_taypsi.infrastructure

• Definitions
  • Body of local closure
  • Variable closing
  • Free variables
• Tactics
• Lemmas
  • Properties of opening
  • Properties of substitution
  • Properties of values
  • Properties of local closure
  • Properties of body
  • Properties of free variables
  • Properties of closing
  • Properties of parallel reduction and local closure

taypsi.lang_taypsi.equivalence

• Lemmas about parallel reduction
  • Properties of oblivious values
  • Substitution lemmas
  • Admissible introduction rules
  • Inversion lemmas
  • Confluence theorem
• Lemmas about expression equivalence
  • Weak head normal form
  • Relation to operational semantics
  • Substitution lemmas
  • Congruence lemmas
• Tactics

taypsi.lang_taypsi.admissible

• Admissible step introduction rules
• Renaming lemmas
• Admissible typing and kinding introduction rules
• Tactics

taypsi.lang_taypsi.inversion

• Kind inversion
• Type inversion

taypsi.lang_taypsi.values

taypsi.lang_taypsi.weakening

• Weakening lemmas

taypsi.lang_taypsi.preservation

• Substitution lemmas
• Other lemmas
• Preservation

taypsi.lang_taypsi.progress

• Lemmas about obliviousness
• Canonical forms
• Progress

taypsi.lang_taypsi.obliviousness

• Properties of indistinguishability
• Obliviousness theorem

taypsi.lang_taypsi.metatheories

• Soundness
• Obliviousness