TODO

[nikivazou]

• 29/4

  • [ ] Read (stainless paper)[http://lara.epfl.ch/~kuncak/papers/HamzaETAL19SystemFR.pdf] to understand
    • [ ] what does it mean for two types to be equal (Niki suspects equality is up to normalization/beta-reduction)
    • [ ] how would application of 3 to foo :: Nat -> () would get accepted
    • [ ] Related: how is subtyping faked in F (see formaliation in (F)[https://dl.acm.org/doi/abs/10.1145/2837614.2837655], (Coq)[https://www.microsoft.com/en-us/research/publication/self-certification-bootstrapping-certified-typecheckers-in-f-with-coq/])
  • [ ] Finish totallity and termination checking on current proof
  • [ ] add type abstraction
    • [ ] on paper
      • [ ] port RJ's definitions
      • [ ] make the proof
    • [ ] in LH formalization
  • [ ] add data types
    • [ ] on paper
      • [ ] port RJ's definitions
      • [ ] make the proof
    • [ ] in LH formalization
  • [ ] start POPL subsmission
  • [ ] outline
  • [ ] port existing formalization

[nikivazou]

In the call Ranjit set the question whether it would be better for the formalization to be ported in Coq. I think @michaelborkowski is very close to finishing and vote to stay in LH. But totally up to @michaelborkowski to make the final decision.