Re: [isabelle] Splicing runtime ML values into Isar
> Can a malicious attacker with access to the ML name space ÂhijackÂ your
> evaluation machinery, e.g. by defining it own structure
> Typed_Evaluation? This is something difficult to handle?
Yes. This may also happen to the "tactic" method:
structure Method = struct
fun set_tactic _ = I
apply (tactic âall_tacâ)
(* exception Fail raised (line 284 of "Isar/method.ML"):
Undefined ML tactic *)
Hygiene is often a problem in languages which support nesting and
(anti)quotation of language elements.
This archive was generated by a fusion of
Pipermail (Mailman edition) and