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



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



> On 7 May 2020, at 23:19, 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.