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

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> 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 (
>, 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.