Stream: Coq users

Topic: Top-down synthesis for library learning


view this post on Zulip Patrick Nicodemus (Mar 20 2023 at 02:16):

Top-Down-Synthesis-for-Library-Matthew-Bowers.pdf
I came across this paper recently and thought it might be interesting to some users here.

In particular I was thinking that it could be interesting to try and refactor a Coq codebase with the approach laid out in this paper. You could go through the Gallina terms and apply these methods and if the approach was successful you might end up with new theorems that generalize existing ones or enabler simpler, shorter proofs.

view this post on Zulip Patrick Nicodemus (Mar 20 2023 at 02:17):

A previous paper from the same research group also looks really fascinating. https://arxiv.org/abs/2006.08381

view this post on Zulip Patrick Nicodemus (Mar 20 2023 at 02:19):

Refactoring the code base in a principled way to expose the most important abstractions underlying the library could make theorem proving much easier.

view this post on Zulip Patrick Nicodemus (Mar 20 2023 at 02:22):

I think there are a lot of papers highly relevant to automated theorem proving i've been missing because they are published under the subject heading "program synthesis". The second paper, DreamCoder, seems like it's potentially very relevant to automated theorem proving by helping a prover keep a reasonably concise list of key theorems it needs to solve the goals.


Last updated: Jun 18 2024 at 08:01 UTC