coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof automation class ideas

From: Talia Ringer <tringer AT illinois.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Proof automation class ideas
Date: Wed, 18 Aug 2021 22:24:39 -0500
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=illinois.edu; dmarc=pass action=none header.from=illinois.edu; dkim=pass header.d=illinois.edu; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=877gaCV17OidCTNWhmVkbrgFvcLGsZoCOD6FR3MRMv0=; b=Hhe4004EBuW/EklVsQPqv+bj2Mv5VPMzcwVCHm2ZOzDsaWaSosXK64/J0VSazBRt8V7hj3+fr+irOaaxv5pJ7RdtrsKyrnQVzP6P46gv/ZbjBK9tX1NbVNyg897opvewLTS8m6uBPpBM11D73xi+ZgZedVznGsXuXB+JrLb5NB0TeVpkNzrv4reT5cEmrgXjTWtUa2oSx8liiZavmhW4xh9AwtyW5E+a4dmKwjlqKmsMbGolUIk8tH3GBpLBmONwV53moteicsIpZNh0nVwzAkF5CjZnPP9KEEd/M91pDgMbfUbQbhHvl3Qv4CUE1rZxmWxSyLWNNuWHEiXuAWXVKA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=mVs7edknXuXwbyMUMDz2mIQSsGaosM6JaOfeFAUSOk1+I0+/aVoiSJd9eFdm0nZ/62f5EkRCbUeQimzCF+RKp6C9PH39Wm9JEqdGJkWtZP4BqJrssURs59XMy/PEek0oRc73TxQDsDpaRyoyootb8IpBBvEBKVuE3WGDPZ/1X81mEDPAU4zqCpJf58pC1I/Ew5K6ch7p7sAkTmDk+OFeS3N1QIJJbMiPWY/4SEQFIymcvPo2fPLhTr86TmViN1PXYX/VsTiMhd9vJ4R+Fn3t/Luu3LmlIE16FLN0zE3A7YUboSJRZ6ZixYlKQaapvgH2fss7XuCjXknTYxmJa9vWqg==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=Neutral smtp.pra=tringer AT illinois.edu; spf=Pass smtp.mailfrom=tringer AT illinois.edu; spf=None smtp.helo=postmaster AT mx0b-00007101.pphosted.com
Ironport-hdrordr: A9a23:GaIyV6tOsARa/CzMklZwwvpk7skCd4Aji2hC6mlwRA09TyXGra6TdaUguiMc1gx8ZJhBo7G90ci7MA7hHPtOi7X5Uo3SOjUO1FHYS72KjrGSvAEIeReOjtK1vJ0IG8MSaKySfCkK/foSizPIaOrIruP3ipxB0ozlvgtQpExRGutdBsRCe2SmO3wzag1PBZ98MoGd6MpBrz/lXXgMdMy0Cj0kcoH41qT2fV7dEHs7Li9izDPLoSKj6bb8HRTd9hACUwlXybNn1WTeiQT26oiqrvn+k3bnpiPuxqUTvOGk5spIBcSKhMRQAjLwijywbIAkf7GZpjg6rMym9V5vutjRpBULOdh19hrqDyyIiCqo/zOl/Ccl6nfkx1PdqXz/ofbhTDZ/MMZFjZIxSGqR12MQ+PVHlI5b1WOQsJRaSTnamj7m2tTOXxZ20mKpvHsLi4co/jxieLpbTIUUgZ0U/UtTHptFNjn98pobHO5nC9yZzOpKcGmdc2vSsgBUsZ2Rt0wIb1W7q3U5y4moO2A8pgE886JY/r1Qop44zuN/d3EejN60dZiB/dp1P7ErhaEUPpZ2fSL4MB2Kffv2ChPhHb3QLtBxB5v8ke+F3FwL3pDeRHUp9up7pH2TaiISiYYNE3ieffFmmqc7vSzlcSGFRjLqxdhZ559l/pPBZJeDC1zadHke1/K6pfMRG8vaXOv2Hql3LbvMEUvCcLw5hjEWkqMiTUU2YYkuo94+H3mHuavwW9HXn92eSu/aIP7BHSstWmbka0FzBwTbFYF790iuHlnigBbqV3ThdleXx+MsLIHqu9ILwIxIDIdLqQR9syXi2v22
Ironport-phdr: A9a23:ckAUlRHyvjr9ngLYKmo8+J1Gf8ZMhN3EVzX9CrIZgr5DOp6u447ldBSGo6k31BmYBM6GtLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys55HfeQFFiCeybb5yLhi9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4TadFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0yVD+/7alkVQXohT8HOTA382/Zl9J+g75Urx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGp2yYJELD+oAJ+lTspXzp1oIrRuxGwasHv7kxzhUhn/s3K061eshHh/c3AE7HtIOtHDUrNTzNKcVUOC117PEwiveYPNLwDrw7pXDfR89r/+WR71wbdbRxlc1FwPDllidrYPoMy6V2+oNs2aV4PZsWOashmMnqgx8ozaiy8Ush4XViIwY107I+CtnzIopONC0VFB2b9CrHZZOtCyXOJd6T8U/SG9roCY30qAKtJG4cSQQ1ZgqxhDSZ+aaf4WG5h/vTvidLDRgiH57ZL6ygwy+/Eugx+HmS8W50VdHojBKn9XRsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU00kKXaJ4I6zbIpipYfrVjPEjP0lUnrkKOaa18o+vCw6+TnZbXmvYOcOJFphQ3kLqsuncm/Dfw5MggIQWeb5fyx2KDs8ED6WrlGk/w7n6fDvJzHK8kWorS1DxFW34o77hawFTam0NAWnXkdK1JFfQqKj5TzO1HPJvD4Aumwg063nTdqw/DGOrzhApPKLnjCi7ftZ6hy5FNByAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiioynkZYdq2017MWbmq5F7JoORa3e33p1+sIFWYD9jA/SuPnkhXWTSRSYXm/RYo94jU6DoWnFsHOSp370+/J5zuyApADPjMOMVuLC3q9L+1stN8NbCaTJMhgiXoJWaXzEufJNDmrpFfwjuI/drKLo3VB84r71N9u++Df0xo18G4sZyx4+2CJS2BymWITATI6wfIlyXE=

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

[Coq-Club] Proof automation class ideas, Talia Ringer, 08/19/2021
- Re: [Coq-Club] Proof automation class ideas, Michael Soegtrop, 08/19/2021
- Re: [Coq-Club] Proof automation class ideas, Adam Chlipala, 08/21/2021
  - Re: [Coq-Club] Proof automation class ideas, Lasse Blaauwbroek, 08/21/2021
    - Re: [Coq-Club] Proof automation class ideas, Adam Chlipala, 08/22/2021
      - Re: [Coq-Club] Proof automation class ideas, Jim Fehrle, 08/22/2021
      - Re: [Coq-Club] Proof automation class ideas, Lasse Blaauwbroek, 08/22/2021
  - Re: [Coq-Club] Proof automation class ideas, Talia Ringer, 08/22/2021
    - Re: [Coq-Club] Proof automation class ideas, Adam Chlipala, 08/22/2021
      - Re: [Coq-Club] Proof automation class ideas, Talia Ringer, 08/22/2021
        
        Re: [Coq-Club] Proof automation class ideas, Adam Chlipala, 08/22/2021