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



> 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.

Tobias





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