Stream: New Members & Projects

Topic: automatic isabelle -> Isar conversion

view this post on Zulip Brando Miranda (Dec 16 2021 at 16:53):

I was curious to know if there was a way to automatically convert Isabelle tactic script to Isar declarative scripts (I know there is no dichotomy but just to phrase the question). Mainly, because I was curious to see if the procedure would teach me anything to do something similar for Coq (to generate IsarCoq lol but that's besides the point, I am genuinly curious about how generate nice Isar like scripts in general and apply it somewhere later). Ideally, it would be nice with a little machine learning if possible. If it does require machine learning then perhaps ideally not deep learning at first (to do such conversions).

Reference: and

Last updated: Dec 07 2023 at 12:30 UTC