coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Prior work on proof assistant performance / optimization
Date: Thu, 07 May 2020 18:32:28 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mailscanner.iro.umontreal.ca
Ironport-phdr: 9a23:i1OLfxQq1/Gw3/7aKKugtGSxYtpsv+yvbD5Q0YIujvd0So/mwa6zZxWN2/xhgRfzUJnB7Loc0qyK6v2mCTVLucfJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRW7oR/Su8ULjoduNqI8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMDE37XzXitdojK1FvB2huxJxw4nRYI6PNfp+eL7WcdcVSGdFW8pcUTFKDIGhYIsVF+cPPfhWoZT+qVsAoxWxBwejC+zzxTJTmn/6wbc33/g9HQzcwAAtGc8FvnTOrNXyMacfSf27zLXWwjXNdfxW3yr25o/PchAnp/GMXKx/cdDMwkQoEgPFiVOQqYrkPzyLzOQAqGmb7/BnVe61lm4nrgZxoj6zxsc2lIbGnIYVxkrY+ipj2Ys4I8CzR0Fnb9C+CpRQqz2aOJVsQsMkW2xmtyg0x6ACtJC0ciYHypcqyRDeZvGGb4SE/hLtWPiMLTl2h39pZbKxihWs/UWkxePyVtW53VdWoidHjNXCuW4B2hrO4caJTft9+12u2TeJ1w3L5eFEIFw0larGK5E62LIwl50TvELeFSH1gEX7lLKae0s69uSy9ejrfrrrqoWCO4J0kA3zMrgiltShDeglMwUCRXWX9OSz2bH580D1WqtGguEonqTfrZvUP94UprSjDA9Qyosj6wiwDzOh0NkAmHkINlNFeBacj4f1IV7OJvb4Aumlg1i2kTdr3ffGMqf8ApXIKXjDlqvhfaxj5EFGzAo/18xQ6IhMBrEAJvL8RFPxucTFAhI3LQC42fjrBMly248ER26CArWVPaPOvVOQ4+IgOeiMZIsbuDbnLPgl4ubjjXo+mV8be6mp3IUYaGqjE/RnOUWZZmDggsoEEWcNuAo+UPbqh0OYXj5XfXq9Q7gz6ikhCI26FYfDWpytgLuZ0SinGZ1Wf3lKBUyIEXf1bIqJQOwMaSKXIs95iDMIT7mhS4k71RGvrgD20bRnLvCHshEf4JnkzZ1+4/DZvRA07z19ScqHgE+XSGQhpX8FSTYwlIV4p0p8x03Lha1/hfpZGMZ75ulOFBo/MpjA1eFzD5b5U1SSLZ+yVF+6T4D+UnkKRdUrzopSMh8sSeXntQjK2m+RO5FQkrWKAJIu9aeFjyrwPcE71nPB0rU7glAiBMBGZzT/2vxPsjPLDouMqH230r6wfP1Mji/X8yGeyG2IoFtVWQo2WqyXBSlCNHuTlszw4wb5d5HrCbkjNVAZm8uLK69RYdTvi1hcAvb5P5LDZmW3h329DBLOzbreNIc=

Hi Jason,

Maybe:

Implementing Typed Intermediate Languages
Zhong Shao, Christopher League, and Stefan Monnier
In Proc. 1998 ACM SIGPLAN International Conference on Functional
Programming (ICFP'98)

It's not directly related to proof assistants, but the techniques
described can be applicable to proof assistants and the experience *may*
be applicable to some extent.

I'd be interested to know what you find,

Stefan

Jason Gross [2020-05-07 18:19:36] wrote:

> 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