Plan

1/2 month - 1 month???

• define a notion of effects as pair of input/S and output/T
• define gtrees as the General type from McBride paper based
• define some primitive effects
  • state
  • recursive calls
  • non-determinism
  • ... see itree paper ...
• try writing some programs with these effects
  • McBride paper
  • itree paper
  • program logics a la carte paper https://pub.ista.ac.at/~msammler/paper/wpitree.pdf
• define + on effects
• define -< (inclusion / subevent) on effects
• define the monad structure
• prove some equalities
• check that one can use GTrees as input and outputs
• think about how to call stuff. E.g. events vs. effects vs. actions vs. ...? gtree vs. itree vs. general vs. ...?

~1month???

• interpretations of gtrees in a composable way similar to section 5 of https://pub.ista.ac.at/~msammler/paper/wpitree.pdf
  • map it to lean monad for execution
  • to an operational semantics
  • to a verification condition / symbolic execution, a bit similar to https://pub.ista.ac.at/~msammler/paper/wpitree.pdf (see eg. Section 3.1)

~1month???

• writing
• buffer

interleaved

• case studies
  • heaplang-like language
  • examples from the itree paper
  • compilation of arithmetic expressions to simple stack language
  • Imp / Asm languages