oadt.base

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

oadt.tactics

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

oadt.ln

• Atom
• Tactics for cofinite quantifiers

oadt.semilattice

• Semi-lattice
• Theorems
• Instances
• Tactics

oadt.prelude

oadt.lang_oadt.base

oadt.lang_oadt.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

oadt.lang_oadt.semantics

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

oadt.lang_oadt.kind

• Definitions
  • Kinds (κ)
• Properties
• Notations

oadt.lang_oadt.typing

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

oadt.lang_oadt.indistinguishable

• Indistinguishability
• Notations

oadt.lang_oadt.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

oadt.lang_oadt.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

oadt.lang_oadt.admissible

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

oadt.lang_oadt.inversion

• Kind inversion
• Type inversion

oadt.lang_oadt.values

oadt.lang_oadt.weakening

• Weakening lemmas

oadt.lang_oadt.preservation

• Substitution lemmas
• Other lemmas
• Preservation

oadt.lang_oadt.progress

• Lemmas about obliviousness
• Canonical forms
• Progress

oadt.lang_oadt.obliviousness

• Properties of indistinguishability
• Obliviousness theorem

oadt.lang_oadt.metatheories

• Soundness
• Obliviousness