Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis

On Wed, Nov 17, 2010 at 1:29 PM, Tobias Nipkow <nipkow at> wrote:
>> Keeping this in mind, I'd like to respectfully request that HOLCF not
>> be referred to as a "logic" -- this seems to imply (incorrectly) that
>> HOLCF uses a different logic than Isabelle/HOL. (This mistaken belief
>> has probably scared off more than a few potential HOLCF users.) HOLCF
>> is no more a distinct logic than are HOL-Word, HOL-Algebra,
>> HOL-Multivariate_Analysis, HOL-Nominal, or any of the other
>> separately-compilable libraries bundled with Isabelle/HOL. I'd much
>> prefer having HOLCF referred to as a "library".
> Hi Brian, that was my doing, I slipped that into Joachim's abstract to
> call attention to the fact that he is using HOLCF. I agree with you and
> felt a little uneasy about the "logic" myself but used it because that's
> the traditional reading of the L in LCF (which I would indeed call a
> logic). But in HOLCF "library" is not a bad reading. Maybe even Library
> of Continuous Functions? Will reword the abstract.

I suppose it's not necessary to completely avoid the term "logic", and
we probably don't need to retroactively change what any acronyms stand
for. But it would be good to distinguish between "logic" and
"formalization of a logic".

For example, HOLCF is a formalization *of* LCF *in* Isabelle/HOL. This
is really just like the situation with HOL-Nominal: While nominal
logic is a real logic, HOL-Nominal is a formalization *of* nominal
logic *in* Isabelle/HOL.

It is a more obvious that HOL-Nominal is built in Isabelle/HOL, since
"HOL-" is a prefix of its name. (Also, it helps that HOL-Nominal
resides in a subdirectory of src/HOL in the distribution, instead of
being adjacent to ZF, FOL, etc. which really are distinct logics from
HOL.) Maybe the same things could help clear up the confusion with
HOLCF? Moving the HOLCF directory would be easy to do. But instead of
just "HOLCF", maybe it could be labeled as "HOL-HOLCF", or "HOL-LCF",
or "HOL-CF"? I suppose I shouldn't take a name-change lightly, though,
since "HOLCF" is a recognized brand. Any suggestions?

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.