Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Usage of HOLCF

Email Gateway (Sep 08 2026 at 11:20):

From: Makarius <makarius@sketis.net>

On 08/09/2026 13:04, Ananthajit Srikanth wrote:

I wanted to know if HOLCF is still in use for any project, or if it is still
maintained.
HOLCF is a regular session within the Isabelle distribution. Thus it is
"automagically maintained", according to the usual quality standards of Isabelle.

I don't know of any recent HOLCF-based projects, but there several entries in
Isabelle/AFP based on it. All of this is "automagically maintained", althouth
the quality standards for AFP are a bit lower than Isabelle.

Makarius

Email Gateway (Sep 08 2026 at 11:27):

From: Ananthajit Srikanth <ananthajit@gmail.com>

Dear all,
I wanted to know if HOLCF is still in use for any project, or if it is
still maintained.

Thanks,
Ananthajit "Ant" S.

Email Gateway (Sep 08 2026 at 11:48):

From: "wolff@lmf.cnrsfr" <cl-isabelle-users@lists.cam.ac.uk>

It is fundamental for the HOL-CSP project and is actually in good shape.

Burkhart

On 8 Sep 2026, at 13:19, Makarius <makarius@sketis.net> wrote:

On 08/09/2026 13:04, Ananthajit Srikanth wrote:

I wanted to know if HOLCF is still in use for any project, or if it is still maintained.
HOLCF is a regular session within the Isabelle distribution. Thus it is "automagically maintained", according to the usual quality standards of Isabelle.

I don't know of any recent HOLCF-based projects, but there several entries in Isabelle/AFP based on it. All of this is "automagically maintained", althouth the quality standards for AFP are a bit lower than Isabelle.

Makarius

Last updated: Sep 17 2026 at 22:43 UTC