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



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





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