oadt.base

• 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
  • Leakage label
  • Expressions (e, τ)
  • Expressions with leakage label (T)
  • Global definitions (D)
  • Global context (Σ)
  • Programs (P)
• Notations for expressions
• More Definitions
  • Indistinguishability
  • Variable opening
  • Substitution
  • Oblivious type values (ω)
  • Oblivious values (v)
  • Values (v)
  • Local closure and well-formedness of expressions
• Notations

oadt.lang_oadt.semantics

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

oadt.lang_oadt.typing

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

oadt.lang_oadt.infrastructure

• Definitions
  • Body of local closure
  • Variable closing
  • Free variables
• Instances
• Tactics
• Lemmas
  • Properties of opening and closing
  • Properties of substitution
  • Properties of values
  • Properties of local closure
  • Properties of body
  • Properties of free variables
  • 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
• Tactics

oadt.lang_oadt.values

oadt.lang_oadt.preservation

• Weakening lemmas
• Substitution lemmas
• Other lemmas
• Preservation

oadt.lang_oadt.progress

• Lemmas about obliviousness
• Canonical forms
• Canonical forms for weak values
• Progress

oadt.lang_oadt.obliviousness

• Properties of indistinguishability
• Obliviousness theorem

oadt.lang_oadt.metatheories

• Soundness
• Obliviousness

oadt.lang_oadt.dec

• Decision procedures
• A naive implementation of step
  • Definitions
  • Correctness

oadt.demo.demo_prelude

• Alternative typing and kinding rules
• Alternative global context typing
• Tactics
• Notations

oadt.demo.int

• Syntax
  • Expressions (e, τ)
  • Expressions with leakage label (T)
  • Global definitions (D)
  • Global context (Σ)
  • Programs (P)
  • Notations
  • Variable opening
  • Oblivious type values (ω)
  • Oblivious values (v)
  • Values (v)
  • Local closure and well-formedness of expressions
• Semantics
  • Weak values
  • Weak oblivious values
  • OADT value typing
  • Evaluation context (ℇ)
  • Small-step relation
• Typing
  • Typing context (Γ)
  • Parallel reduction
  • Expression equivalence
  • Typing and kinding
  • Global definitions typing
  • Program typing
• Infrastructure
  • Body of local closure
  • Variable closing
  • Free variables
  • Tactics
  • Lemmas
• Decision procedures

oadt.demo.int_prelude

• Alternative typing and kinding rules
• Alternative global context typing
• Tactics
• Notations

oadt.demo.demo1

oadt.demo.demo2

oadt.demo.demo3

oadt.demo.demo4