Email Gateway (Aug 23 2022 at 09:08): Email Gateway (Aug 23 2022 at 09:08):From: Konrad Slind <konrad.slind@gmail.com>
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
Last updated: Apr 19 2024 at 01:05 UTC