[TYPES] Type systems for cryptographic proofs

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi all,

I'm curious what work there is about type systems that encode cryptographic
proof systems, like zero knowledge proofs and witness indistinguishable
proofs. These proof systems have well-defined soundness and completeness
criteria. The criteria are probabilistic, but I do not think that should be
an issue given the work on probabilistic PL in recent years. If there are
any papers on this topic, I would super appreciate some pointers.

Thanks,

Talia