Tasks.md

Tasks

STLC and learning

• Read sections 1-4 in note by Lau
• Define type safety for STLC
• Define Logical Relations for type safety for STLC
• Prove the two intermediate lemmas
• Read parts I and II of types and programming languages
• Watch videos on Blackboard

System F. The Language

• Write in language (System F) in report
• Add explaining text to each part
• Define and prove "Evaluation under Context" lemma for System F w/rec
  • Define k = [] or Val(e) lemma. Show 1 case
  • Write in complete EuC lemma
  • Proof read
• Refactor for terminating language
• Substitution
• Normalisation
• Determinacy
  • For one step
  • Multi-step evaluation to a value.
• Fix type-setting

Contextual Equivalence

• Define Contextual Equivalence for System F
• Write in Contextual Equivalence
• Explanation and intuition
  • Talk about CE being enough for integers
  • Talk about CE being enough for non-base types (specifically function type)
    • Show congruence rule for function application, and argue it's correctness, and why it is enough (see google photos)
• Mention the other, equivalent way of defining Contextual Equivalence (see google photos)
  • Congruence Rules
  • Adequacy
  • Prove they are equivalent
    • ctxeq(forallC) => congruence (we showed one rule) and adequate (google photo)
    • other direction: (google photo)
      • main proof
      • define helper lemma
      • prove helper lemma
        • define reflexivity lemma
        • prove reflexivity lemma
          • show one case (Tlam)
        • show cases
          • base [*]
          • add
          • fst
          • rec
          • app
          • Tlam
• Fix type-setting
  • ctx-equiv -> CE
  • type environment and variable environment (tctx -> venv)
  • refactor judgements
• Define Congruency and Adequacy as separate properties
  • In case of reflexivity and Lemma 6, state only for relations having congruency (and possibly well-typedness).
• Refactor for terminating language
• Finish writing text
• Fix type-setting

Logical Relations

• Define a logical relations model for CE
• Write in LR
  • val- and exp-interpretation
  • varenv- and typenv-interpretation
• Prove compatibility lemmas (only unit and add with well-typedness)
  • Unit
  • Add
  • Match (if-similar, but simpler)
  • Fst
  • Lam
  • App
  • Tlam
  • Tapp (if space)
• Show results about LR
  • LR => Ctx
    • adequacy
    • congruency
  • Fundamental theorem
• Finish writing text
  • Section 4.1 Logical relations
  • Section 4.2 Defining the LR Model
  • Section 4.3 Compatibility lemmas
  • Section 4.4 Properties of LR
• Fix type-setting

Using the Logical Relations

• Identity
  • Identity derivation
    • write in theorem
      • empty environments
    • prove it
  • Identity contextual equivalence
    • write in theorem
      • general environments
    • prove it
      • the proof itself
      • determinacy
        • State it (in language chapter)
      • substitution preserves typing
        • prove it
• Empty type
  • write in theorem
  • prove it
• Idempotency
  • write in theorem
  • prove it
• Commutativity
  • write in theorem
  • prove it
  • check correctness
• Lam hoisting
  • write in theorem
  • prove it
  • check correctness
  • Well-typedness
    • build expression from assumptions and then fund thm.
• Finish writing text
  • Identity
  • Empty type
  • Idempotency
  • Commutativity
  • Lam hoisting
• fix type-setting

Report Writing

• Appendix
• Write introduction
• Write conclusion and ideas for future work
• Write abstract
• Proper references
  • get your bibtex entries from \url{https://dblp.org/}
• Fix annotated mistakes
  • remove contractions
  • add superscript R to relations
  • rewrite explanation of expression relation
  • rewrite section 4.1
• Shorten report
  • chapter 2
  • chapter 3
  • chapter 4
  • chapter 5
• Format appendix
• Proofread report

Exam period

• Watch exam video on Blackboard
• Read parts of types and programming languages again
• Read Theorems for free!
• Skim through notes by Lau
• Make slides (for 15 min)