*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, 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 13:02:22 -0800*In-reply-to*: <4CE3FA2E.3090803@in.tum.de>*References*: <4CE3FA2E.3090803@in.tum.de>*Sender*: huffman.brian.c at gmail.com

On Wed, Nov 17, 2010 at 7:52 AM, Tobias Nipkow <nipkow at in.tum.de> wrote: > by Joachim Breitner > > In his dissertation, Olin Shivers introduces a concept of control flow > graphs for functional languages, provides an algorithm to statically > derive a safe approximation of the control flow graph and proves this > algorithm correct. In this research project, Shivers' algorithms and > proofs are formalized using the logic HOLCF in theorem prover Isabelle. > > http://afp.sourceforge.net/entries/Shivers-CFA.shtml > > Enjoy! It is great to see new AFP entries using HOLCF. This one is a nice example of how HOLCF can be used for part of a development where much of it is done directly in ordinary Isabelle/HOL; in this case the HOL set type is made into a cpo, so that 'fixrec' can be used for recursive definitions of sets. I'd like to encourage more of this kind of cross-over between Isabelle/HOL and HOLCF, and remind all the potential users of HOLCF out there that the barrier to entry is probably not as high as you think: HOLCF is just a library of definitions, theorems and packages that you can import from Isabelle/HOL if you need it; you don't have to abandon all of your Isabelle/HOL theories if you want to try using HOLCF. 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". Thanks! - Brian

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

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

- Previous by Date: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis
- Next by Date: Re: [isabelle] NEW AFP entry: Shivers' Control Flow Analysis
- Previous by Thread: [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