Gotta prove fast

Stream: lean4

[Richard L Ford]

I notice that @Sebastian Ullrich is giving a talk on Saturday titled "Gotta prove fast: building an ecosystem for effortless native compilation of tactics". I won't be able to attend and wonder if there is a preprint for this talk. Also I was wondering if any of the code for this is publicly available. I'd be interested in seeing it.

[Sebastian Ullrich]

All POPL tracks will be available on YouTube I believe. The most relevant PRs are https://github.com/leanprover/lean4/pull/795 and https://github.com/leanprover/lean4/pull/949 (the final glue).

[Richard L Ford]

Thanks for the information. I look forward to hearing the recorded talk .

[Siddhartha Gadgil]

Any updates on this (I could not find a recorded talk)?

[Henrik Böving]

I did watch it live over here https://www.youtube.com/channel/UCwG9512Wm7jSS6Iqshz4Dpg/videos (was very cool btw^^) so I would expect the snippet of the overall stream to eventually get published on this channel? It has lots of other POPL talks after all.

[Sebastian Ullrich]

Yes, it should get published there eventually

[Eric Taucher]

Is it just me or did others wonder into this topic thinking some student was expecting a homework answer only to find this? Maybe the title should be changed as this looks interesting but the title is leading other to skip this topic because they are thinking what I thought.

[Sebastian Ullrich]

That didn't occur to me before, but I love it.