The Coq mailing list

[Lawrence Dunn <dunnla AT seas.upenn.edu>]

Hi Talia,

I have some yet unpublished work that uses string diagrams to reason about operations on syntax with variable binding, which is formalized in Coq. The development workflow for many proofs consists of visually manipulating string diagrams and then translating these (rather tediously) to rewrites in Coq. An example of such a string diagram can be found in the git README here: https://github.com/dunnl/tealeaves

Some proofs whose structure is more readily visualized by manipulating string diagrams is found in this file:

https://github.com/dunnl/tealeaves/blob/master/Tealeaves/Singlesorted/Classes/Bimonad.v

Unfortunately I don't have a paper to point to yet, perhaps in the next few months or so. Maybe you will find it relevant anyway.

Warm regards,
Lawrence

On Sun, Nov 14, 2021 at 11:28 AM Cyrus Omar <comar AT umich.edu> wrote:

I don't have a particular idea, but you might want to reach out to Katherine Ye at CMU, whose work on Penrose is all about domain-specific visual representations of mathematical structures.

If you want these visual representations to be interactive, we've been doing some work in that area in the context of functional programming: https://hazel.org/papers/livelits-paper.pdf.

Cyrus

On Sat, Nov 13, 2021 at 10:28 PM Ralf Jung <jung AT mpi-sws.org> wrote:

Hi Talia,

I am not sure if that is what you are looking for, but "Ribbon proofs" is an
interesting way to visualize the structure *of* a proof:
https://johnwickerson.github.io/papers/ribbons_esop13.pdf
The paper formalizes the "syntax" of these visualizations and proves things
about them.

; Ralf

On 13.11.21 20:06, Talia Ringer wrote:
> Hi all!
>
> I had a fun idea today for programmable neurosymbolic proof automation based on
> domain-specific visual representations of structures. By visual representations
> I mean representations like those seen in this blog post:
> https://www.daniellitt.com/blog/2020/12/26/the-geometry-of-the-sylow-theorems
> <https://www.daniellitt.com/blog/2020/12/26/the-geometry-of-the-sylow-theorems>
>
> I'm really curious if people have other domain-specific visualizations of
> structures they reason about in proofs, especially if coupled with formal proof
> developments! I'm extra curious when you use the visualization to reason about
> the proofs by hand, but encode them formally in a proof assistant. I'm extra
> extra curious if the visual representation is of a structure used inside of a
> program, and not "just" a mathematical proof, but I'm very open to both.
>
> If you do, I'd love examples!!! This idea is like a couple of hours old, but I
> want to write it up with some examples so I can get a sense of how tractable it
> is, and probably propose it to some students next year.
>
> Thanks!
>
> Talia

--
Website: https://ralfj.de/research