[TYPES] Type systems for cryptographic proofs

[Talia Ringer]

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