Josh Chen (Oct 15 2019 at 20:45): Josh Chen (Oct 15 2019 at 20:45):This is something I've been working on for a little while, and I'd like to make it public on here to see if there's interest in the concept, and also maybe if I can find collaborators to work on this with.
Idea:
I'd like to see an Isabelle instantiation that provides a dependently-typed environment for proof development. Essentially, "Coq/Lean/Agda mode" for Isabelle, befitting its claim as a generic proof assistant. This is certainly a long-term goal, but I'm hopeful that a proof-of-concept would be achievable within the next year or so, if nothing else gets in the way.
The idea of deeply embedding dependent type theory in HOL is not new, and is relatively straightforward (see for instance https://doi.org/10.1007/bfb0037108). There's also of course the CTT object logic from the early days. But these works use extensional equality with no universes. Formulating a theory with intensional equality with some form of universe hierarchy, which seems indispensable in order to formalize particular parts of mathematics, is a little more work and is what may be nice to see done in Isabelle.
I started working on this in my Masters when I knew nothing about Isabelle, and have recently picked the idea up again. The main issues I've encountered so far have been in formulating universes in a coherent and convenient way, integrating the type-theoretic style of reasoning with Isar, and in notational and term elaboration infrastructure. I've made some nice progress on some things which I can describe if there's interest, and the work so far is online at https://github.com/jaycech3n/Isabelle-Spartan.
In any case, I'd greatly appreciate the community's thoughts about any part of this: how you might see yourself using dependent types if Isabelle had them, what features would be helpful, and generally in which directions this should go in order to be useful and valuable. :)
Kevin Kappelmann (Oct 15 2019 at 23:12):Hey Josh, I am interested but rather busy at the moment. I did take a note to have a look at it to give you feedback. this might take a few days though (I think this week is out of scope). anyway, if you feel comfortable about the state of your project already, you might wanna post it to the isabelle users e-mail group too.
Josh Chen (Apr 06 2020 at 11:36):I now have a preprint online describing the state of this project: https://arxiv.org/abs/2002.09282, or https://joshchen.io/pdf/Isabelle-Spartan.pdf for the latest version with a version with updates+corrections in the works.
Isabelle/HoTT (https://github.com/jaycech3n/Isabelle-HoTT) has been updated and reorganized too! Automation is quite rudimentary so proofs can be a little verbose, but already it's able to prove nontrivial things quite nicely.
Other features e.g. typeclasses, inductive types etc. are not yet there, and I'm planning to work on a cubical type theory flavor for Isabelle/HoTT, so there are quite a few places one could jump in if one were interested to work on this!
Lawrence Paulson (Nov 02 2020 at 16:58):Your second link is a 404
Josh Chen (Nov 02 2020 at 17:12):Fixed, thanks!
Last updated: Dec 21 2024 at 20:18 UTC