Qiyuan Xu (Sep 05 2022 at 11:25): Qiyuan Xu (Sep 05 2022 at 11:25):The type system of Isabelle is restricted. Simple-typed lambda calculus is too limited. It is a well-known deficiency compared with CoC-based PAs like Coq. Any deep user of Isabelle feels this restriction I believe.
We cannot make a generic shallowly-embedded semantic framework, whereas, in CoC, one can simply let terms bind types to make that, like datatype generic_model = Constructor (t:Type) t and the Constructor has type .
Maybe, by heavily using predicates, the nature of Isabelle doesn't need types to bind terms, but, it's perhaps significant to allow terms to bind types, to achieve the generic framework as mentioned above.
There is an extension of HOL4 that implements , named HOL-omega. They claim existing proofs of original HOL4 can be retained on HOL-omega, and also all inference rules, though I'm not sure whether tactics and automation can also be retained. It seems to be a feasible approach for us because we have a similar logic foundation (for Isabelle/HOL).
Maybe, experts, we can discuss this approach. Would it be hard? What are difficulties we might meet?
Qiyuan Xu (Sep 05 2022 at 11:35):see https://en.wikipedia.org/wiki/Lambda_cube
Kevin Kappelmann (Sep 20 2022 at 11:32):Some time ago, I briefly chatted with @Lukas Stevens about this. Maybe there would be some theoretical subtleties (e.g. due to Isabelle's typeclasses), but I think the main problem would be that you would have to change almost every piece of ML code.
Last updated: Apr 25 2024 at 04:18 UTC