[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
One relevant reference would be Noam Zeilberger's exploratory work on "a type-theoretic understanding of zero-knowledge" presented at the HOPE workshop (Higher-order Programming with Effects) 2012 https://software.imdea.org/~noam.zeilberger/talks/hope2012.svg (As far as I am aware there is no article/detailed version of this work.) On Mon, Jan 25, 2021 at 9:14 AM Talia Ringer <trin...@cs.washington.edu> wrote: > [ 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 >
