(no subject)

Date: 2024-11-28 05:02 pm (UTC)
purplecat: An open book with a quill pen and a lamp. (General:Academia)
From: [personal profile] purplecat
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.
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

Profile

purplecat: Hand Drawn picture of a Toy Cat (Default)
purplecat

June 2025

S M T W T F S
1234567
8 9 1011 12 13 14
15 16 17 18 19 20 21
22 23 24 25 26 2728
2930     

Tags

Style Credit

Expand Cut Tags

No cut tags