*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 17 Nov 2010 14:07:36 -0800*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4CE4492E.8090506@in.tum.de>*References*: <4CE3FA2E.3090803@in.tum.de> <AANLkTikhvPKh7QmGp3Z4B1EbN5-RtiF4GTL0z37dH-e0@mail.gmail.com> <4CE4492E.8090506@in.tum.de>*Sender*: huffman.brian.c at gmail.com

On Wed, Nov 17, 2010 at 1:29 PM, Tobias Nipkow <nipkow at in.tum.de> 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

**Follow-Ups**:**Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis***From:*Jasmin Blanchette

**References**:**[isabelle] NEW AFP entry: Shivers' Control Flow Analysis***From:*Tobias Nipkow

**Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis***From:*Brian Huffman

**Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis
- Next by Date: Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis
- Previous by Thread: Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis
- Next by Thread: Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis
- Cl-isabelle-users November 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list