We present the syntax and the proof system of matching logic and introduce the research problem of producing succinct cryptographic proofs for checking matching logic proofs, aka Proof of Proof.
This technical report was first published on Chen’s personal GitHub repository at https://github.com/xc93/pi-square-doc/commits/main/mlzk.pdf in June 2023. The idea of achieving verifiable computing via combining mathematical proofs and cryptographic proofs was firstly explained by Roşu in his presentation The K Approach and Vision in 2020; see slide 99 of the slide deck at https://drive.google.com/file/d/1iXda2NyGzKVWxkd02IlXj5Tq5cOM_gNd/view. We thank Don Beaver and Rahul Maganti for early brainstorming on the Proof of Proof ideas and algorithms.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
