On 08/06/2016 15:01, ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ wrote:
Dear Tobias and Makarius! Thank you for your links and suggestions. Now I realize that it's better to import my objects to ML directly. I will concentrate on this approach. I have a question regarding "eval" proof method. If one uses "eval", what stack of code will one have to trust? Will the "trusted base" be larger than that for proofs without "eval"?
Yes, you also need to trust the translation of HOL function definitions into ML function definitions.
If you can give any links discussing the topic of trusted code stack in theorem provers (whether in case of "eval" method or not) â I would appreciate it. Thank you! Stanislav.
Description: S/MIME Cryptographic Signature