log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
PLunch: A tour-de-force in Coq Automation
Leonidas Lampropoulos
Zoom
Monday, April 27, 2020, 12:00-1:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract
I'll talk about different ways of automating Coq proofs, with an emphasis on the "repeat match goal with" paradigm that Adam Chlipala has popularized. Most of the material will be based on Adam's first lecture in the 2017 DeepSpec Summer School, and we'll go over creating our own "tauto" and (more ambitiously) dealing with quantifiers in a principled style.

Zoom link will sent via PL Reading mailing list.

This talk is organized by Sankha Narayan Guria