coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Prior work on proof assistant performance / optimization

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>, agda-list <agda AT lists.chalmers.se>, Coq Discourse <coq+miscellaneous AT discoursemail.com>, lean-user <lean-user AT googlegroups.com>, cl-isabelle-users AT lists.cam.ac.uk
Subject: [Coq-Club] Prior work on proof assistant performance / optimization
Date: Thu, 7 May 2020 18:19:36 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f65.google.com
Ironport-phdr: 9a23:vN5+SBfYsVVadUlZYtI2jRHBlGMj4u6mDksu8pMizoh2WeGdxc26bBeN2/xhgRfzUJnB7Loc0qyK6v2mCTVLucnJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRW7oR/Su8ULjoduNqQ8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUStODJ6hb4sUF+oOI/pXr5XzqVsJqBuxHwisBOXywTNMiXL72ag23uI8Gg/EwQMgBcoDv3varNr3NKkcX+O7wrTWwzrfdP5Zwyvx5ZLSfxw9vf2BX7R9etfRx0k1EAPFi02dp4j/MDOO0eQNtXWQ4et6VeKokG4nsBx6rz+txsg2kYnJgYQVyl/e9SV+24Y1Ptm1RVV0Yd6hCpRQtiWaO5FqTcMlRmFloSA3waAJtpCnZiYF0ognxwLBZPyddYiF+gzvWuiNLDl4hH9pZLayigqz/EWu1+DxVsi53UtWoiRLj9TBuG4B2hPQ58aIS/Zz8Vms1CuP2Q3T9+xJIF04mLbdJpU8zLAwkZ8Tvl7CHi/wgEj2g66Wdlkk+ui18OvreLTmppiaOoRpiQ/+KrwjltKjDek8KAQDXGiW9f6i2LH+/kD1WrRHg/0wn6LEqp7VP94bqbS8AwJN0oYs9RK/DzC+3dQdh3YHLVZFdAuZgIjrJl3COf74APa/jli2nzdrwPfGPrLlAprTNHTMjLDhfbNl505dzgo808xf6opKBr0dJP//QEz8udzCAhMnLgC5wPzrBdR9248GXGKAGK6ZMKfcsV+S4eIvJvGBZI0PtzbmLPgl4fHujWU+mV8GZqmk2YAaaH+9Hvt8IkWZZWDgjcsGEWcPpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDxXHYSmHoQmzFSlsBLwg+5sKfOR8SkFv7ri0sJ07qvdj0d2vTV7A83Y12CWUykgl2wEThcy3btjugp2yl6H1KVimLpDGIoXr9hOS08WNIXXyPFgEN26DgnGZ5SMSU2tT9GiCDc8Sc8q69MPeE16Bs+5gxXK3i7sCLgQwfjDAJE99OfBxHXrb5J5xn/AkbQ6gkMOTcxIOmmribR46hDIQYXOlhPd362uMKUH1STA8GOOiHeVsVtDeApxSrneG3sWYw3fppLk5RDsVbirXJYuKQxHgeGYLbBRIonrhE5BQvj5P8/FMkq+nm6xAVCDwbbaP9miQHkUwCiIUBtMqAsU53vTcFVnX3vzkyflFDVrUGnXTQb06+An8SG0S0Y1y0eBaEgzj+PkqC5QvuSVTrYo5pxBvS4grztuG1PkhoDZDtOBo0xqe6AOOIpgsmcC7nrQsklGBrLlL61mgQRDIQF+vker2hcuT4sezI4lq3QlyAc0IqWdggtM

I'm in the process of writing my thesis on proof assistant performance bottlenecks (with a focus on Coq). I'm having some trouble finding prior work on performance engineering and/or benchmarking of proof assistants (other than the paper on the Lean tactic language (https://leanprover.github.io/papers/tactic.pdf)), and figured I'd reach out to these lists.

Does anyone have references for prior work on performance analysis or engineering of proof assistants or dependently typed languages? (Failing that, I'd also be interested in papers about compile-time performance of compilers.)

Thanks,

Jason

[Coq-Club] Prior work on proof assistant performance / optimization, Jason Gross, 05/08/2020
- Re: [Coq-Club] Prior work on proof assistant performance / optimization, Stefan Monnier, 05/08/2020
- Re: [Coq-Club] [Agda] Prior work on proof assistant performance / optimization, András Kovács, 05/08/2020
  - Re: [Coq-Club] [Agda] Prior work on proof assistant performance / optimization, Stefan Monnier, 05/12/2020
    - Re: [Coq-Club] [Agda] Prior work on proof assistant performance / optimization, András Kovács, 05/12/2020
      - Re: [Coq-Club] [Agda] Prior work on proof assistant performance / optimization, Wolfram Kahl, 05/12/2020
  - Re: [Coq-Club] [Agda] Prior work on proof assistant performance / optimization, Jason Gross, 05/14/2020
- Re: [Coq-Club] [isabelle] Prior work on proof assistant performance / optimization, Lawrence Paulson, 05/08/2020
- Re: [Coq-Club] [isabelle] Prior work on proof assistant performance / optimization, Konrad Slind, 05/14/2020