The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> 12, 13: building usable automation

Not sure if it's covered by "usable", but I think building scalable (in the performance sense) and maintainable automation are also quite important.

On Sat, Aug 21, 2021, 15:24 Jules Jacobs <julesjacobs AT gmail.com> wrote:

Maybe this is too basic given the list of what you are planning to teach but I enjoyed looking into the paper that Coqs tauto tactic is based on according to the docs: 

Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic, September 1992.

On Thu, 19 Aug 2021, 09:09 Talia Ringer, <tringer AT illinois.edu> wrote:

Hi! It has been a while. I'm thinking a bit ahead to the grad seminar I'll teach in the spring (starting in January) which I think I'll have complete freedom over. I really want to do a proof automation course, where one day every week is a deep dive on a single paper, and the other is hacking on the paper artifact. I was thinking this outline:

1: getting started

2, 3: languages for automation (including reflection)

4, 5: custom tactics & decision procedures

6, 7: plugins & transformations

8, 9: ATP for ITP

10, 11: neural networks for proofs

12, 13: building usable automation

14: what's next?

I'd really like feedback from folks in the community about whether I'm missing any big topics (I could feasibly condense 2-5), whether there are papers you'd really like to see for some of these topics, and whether there are guest speakers you'd recommend for any of these weeks. I'll probably invite a few if I can.

Talia