my proposed research direction is indeed a trinity. in particular:
0. proof-objects
1. operational semantics
2. categorical semantics