|
|
|
|
|
|
by momentoftop
22 days ago
|
|
|
Isabelle is still a very active LCF proof assistant, and it's still written in Poly/ML. It's pretty aggressively concurrent under the bonnet, and leverages Poly/ML well for that. There's still HOL4, which predates Isabelle and is still going, and it also recommends using Poly/ML. I mostly worked with HOL Light which started as a CAML project and now runs on OCaml. |
|
|