[TYPES] Type systems for cryptographic proofs

[Gabriel Scherer]

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 <tringer at 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
>