Re: [TYPES] Type systems for cryptographic proofs

Mads Buch <me-dCzsxaMYwglWk0Htik3J/[email protected]> Mon, 25 Jan 2021 09:20:01 +0000
Newsgroups gmane.comp.science.types
Message-ID <RGNHYFk22i7UUhte9FZ8Izci184lr2Tbbnm-uIMh-uvQ8Xrz1Acw2FRWzVUnGgL-Dz967SNZfTHY8MQttjIu1L0XxX1ScP26TWG21s-mjh8=@madsbuch.com>
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Talia

A quick reference to mention is EasyCrypt:

https://www.easycrypt.info/

I used it in my masters thesis for differential privacy but it is geared towards cryptographic proofs using probabilistic reasoning techniques.


Venlig hilsen
Mads Buch

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Sunday, 24 January 2021 21:06, 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