Syntactic type system for heap_lang
@dfrumin defined a syntactic type system for heap_lang in the reloc repo:
https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v
I would like to use his type system to state the fundamental theorem for the unary logical relation of heap_lang in iris-examples (https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logrel_heaplang), as right now that formalization only has semantic types and the semantic typing rules.
How about adding @dfrumin's syntactic type system to the heap_lang folder of the Iris repo?
Some things to discuss:
- It currently relies on autosubst. Using strings for binding in types will be horrible, since there we actually have to deal with capture. Do we mind having a dependency of Iris on Autosubst, or would it be better to write a manual version with De Bruijn indexes?
- It uses some fun encodings for pack and unpack (of existential types) and type abstraction and application, see https://gitlab.mpi-sws.org/iris/reloc/blob/master/theories/typing/types.v#L80 Are we happy with that, or are there more elegant ways of doing that?