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)

https://link.springer.com/chapter/10.1007/3-540-44659-1_2


https://www.researchgate.net/publication/2390013_Efficiency_in_a_Fully-Expansive_Theorem_Prover

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

https://www.cs.utexas.edu/~kaufmann/itp-trusted-extensions-aug-2010/summary/summary.pdf




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
>



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