Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Konrad Slind <konrad.slind AT gmail.com>
  • To: Jason Gross <jasongross9 AT gmail.com>
  • Cc: 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: Re: [Coq-Club] [isabelle] Prior work on proof assistant performance / optimization
  • Date: Thu, 14 May 2020 13:30:17 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=konrad.slind AT gmail.com; spf=Pass smtp.mailfrom=konrad.slind AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f46.google.com
  • Ironport-phdr: 9a23:Mi7c7RdvBgBHwYfve2YgQh8ilGMj4u6mDksu8pMizoh2WeGdxc26ZR2N2/xhgRfzUJnB7Loc0qyK6v2mCDJLuM/d+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLssQbgIRuJrssxhbGv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/XrJgcJskq1UvBOhpwR+w4HKZoGVKOF+db7Zcd8DWGZNQtpdWylHD4y7coUPEvEBPf5GoIbhu1sAoxy+BQy2C+PuzD9Dm3v60KI+3ugkFwzNwQ4uEM8UsHnMo9r1OqUdX+C7wqfL0DvNce9Z1Czn54TUaB0su+2AUa5yfMfX1EIhFxnFjlKVqYH9Oj2V0eINs3KB4OV9SOmhlmonqwB3ojey28whjYrJhoUTylDe7yp23Zw5Jca8SE56Z96rDYBdty6fN4RsQ8MiR3tktzo9yr0DoJO2ejUBx5s7yRDFcfOHb5SI7Qz5VOaXOTp1hmxodrKhixqs8UatzvPwWteq3VtXqidIncXBuH4D2RHQ98SLVvVz80Wj1DuB1Q3d6uNJLF4pmabHJJAt3KI8m5wOukrNGS/2nV/5jK6Qdkg84eio8/7nYrTgpp+TKYB0kBvyPbgpmsy6Geg4KBYBX3OF9uumzr3s4U35QLpQgf0qjKbVqpbaKtoHpqKhHg9Vzpgs6hmlADe9ytgXg2QILE9ddBKIjojpJ1HOIO3jAvulglSslzFmzO3FML35GpjBMGTPnbP7cbt+60NQ0hQ/wcxc6p5OBbwMIfT+UVLrutPCFB82KQm0zv7nCNpj0oMeXnqCAqqDP6PTtV+E//wgLPSRaIMMtjbwJPko6+ThjX8+nl8dcq2p0oUNZH+kGfRmJl2VYXvqgtgfDWcHphQyQPDuhVGYUjNeZ2y+U7wg6jw4Eo6rAobOSpiogLOb3Se7GpNWZnpBClCJCXrodIKEW/EWaC2IP8BtiCcEVbygS48nyB6jrwD6y799IerV/i0Ur47s1N9w5+HLjxE96SR0D9iB02GKV2x7gmQIRyYv0K9jpUx910yM3LNjg/1YENxT/+lGXh07NZ7a1ex6Csr9VhjPfteTGx6aRYCECCo2SJoe2dgVeA4pGdy5iRbMxS2xGO49mLmCBZhy+aXZiSvfPcF4nlXB0rMogxEdRspJOSXyhal57QHfQZXNkkOVv6mvfKUYmiXK8THQniK1oEhEXVsoAu3+VncFax6T8I2gtxHyCoS2ALFiCTNvjMuLK69EcNrs1AwUS/LqOdCYaGW0yT7pWUS4g4iUZY+vQF0zmT3HARFdwQ8W9HeCcwM5A3X5+j+MPHlVDVvqJnjU36x+pXe8FBJmygiLawhs2+Pw9EJLw/ObTPwX0/QPvyJz8zg=
As Larry said, there has been a lot of work on this over the years. A few references off the top of my head (slightly HOL-centric)



Related to this is work on sound interfaces to external tools, also an enduring topic:




On Fri, May 8, 2020 at 4:08 AM Jason Gross <jasongross9 AT gmail.com> 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

Archive powered by MHonArc 2.6.18.

Top of Page