purplecat: An open book with a quill pen and a lamp. (General:Academia)
purplecat ([personal profile] purplecat) wrote 2024-11-28 05:02 pm (UTC)

I also experimented with Isabelle since it had a formalisation of conduction. The interface has improved massively since then, with a much more intuitive "assuming X then Y follows by Z" kind of syntax which Xin was exploiting (I don't honestly think he had much understanding of the details of Isabelle - Z was generally blast (one of the built-in automated reasoning algorithms).

Larry handed over most of the development of Isabelle to Tobias Nipkow while I was still in Edinburgh (or possibly Tobias just gradually took it on - certainly by the turn of the century I'd say Tobias was clearly driving much of the development). I'm not sure who is running it now, digging around the details of Isabelle 2024, suggests Larry and Tobias are still overall in charge but most of the development work is being done by others and there is some organisation called Isabelle CTO that seems to coordinate this in some way.

Post a comment in response:

This account has disabled anonymous posting.
(will be screened if not validated)
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting

If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org