Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Prior work on proof assistant performance / op...

Email Gateway (Aug 23 2022 at 09:05):

From: Jason Gross <jasongross9@gmail.com>
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

Email Gateway (Aug 23 2022 at 09:06):

From: Lawrence Paulson <lp15@cam.ac.uk>
In the case of Isabelle, performance analysis has always been part of the development process and we keep an eagle eye on the runtimes in our nightly builds. Much of this is routine software engineering rather than research. But then there’s all of Makarius’s work on multithreading...

Larry Paulson

Last updated: Nov 21 2024 at 12:39 UTC