[TYPES] Type systems for cryptographic proofs

[Jelle Herold]

Underappreciated topic!

There is Anton Golov's master thesis where game theoretic proofs are
implemented in Agda.
http://dspace.library.uu.nl/handle/1874/367810

And more sketchy & categorical, but could be adopted to type theory:

Izaak Meckler wrote down some idea's on categorically viewing crypto, which
could be interesting.
https://math.berkeley.edu/~izaak/research/documents/Categorical-Cryptography.html

We have been thinking about doing cryptography using surface diagrams, I
believe a discussion between Fabrizio Genovese and Amar Hadzihasanovic and
can be found here
https://categorytheory.zulipchat.com/login/#narrow/stream/229156-applied-category.20theory/topic/cryptography
(sorry can not log in right now to check)

Best,
Jelle.

On Mon, Jan 25, 2021 at 9:15 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
>