[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 >
