[ ] Implement untyped plutus core (syntax/operational semantics)
[ ] Implement typing, should be very similar to typed PLC, but no annotations on the term, everything in the derivations
[ ] recover typing for UPLC: typing_PLC_UPLC : lower t t' -> ... |-PLC t : T -> ... |-UPLC t' : T
[ ] Prove that there is a bisimulation between CEK machine and (small-step?) operational semantics (see https://www.cs.cmu.edu/~fp/courses/15814-f19/lectures/13-bisimulation.pdf)
[ ] Prove that typed and untyped plutus core correspond
jaccokrijnen
commented
1 year ago
Some ideas of what we could do:
[ ] Implement untyped plutus core (syntax/operational semantics) [ ] Implement typing, should be very similar to typed PLC, but no annotations on the term, everything in the derivations [ ] recover typing for UPLC:
typing_PLC_UPLC : lower t t' -> ... |-PLC t : T -> ... |-UPLC t' : T[ ] Prove that there is a bisimulation between CEK machine and (small-step?) operational semantics (see https://www.cs.cmu.edu/~fp/courses/15814-f19/lectures/13-bisimulation.pdf) [ ] Prove that typed and untyped plutus core correspond