Email Gateway (Aug 18 2022 at 16:28): Email Gateway (Aug 18 2022 at 16:28):From: Tobias Nipkow <nipkow@in.tum.de>
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!
Email Gateway (Aug 18 2022 at 16:28):From: Brian Huffman <brianh@cs.pdx.edu>
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!
Email Gateway (Aug 18 2022 at 16:28):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 16:28):From: Brian Huffman <brianh@cs.pdx.edu>
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?
Email Gateway (Aug 18 2022 at 16:28):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
The name HOLCF is nice and established, and the main issue is the confusing directory structure. Fixing the directory structure would yield "~~/src/HOL/HOLCF" and "HOL-HOLCF".
Jasmin
Email Gateway (Aug 18 2022 at 16:28):From: Brian Huffman <brianh@cs.pdx.edu>
Having the heap image named "HOL-HOLCF" sounds good to me; I will
continue to use just the name "HOLCF" in all the internal
documentation, though.
I would also like to address the positioning of HOLCF in the online
documentation. Currently it is listed on each of these pages:
http://isabelle.in.tum.de/documentation.html
http://isabelle.in.tum.de/dist/library/index.html
where all of the other entries are really distinct logics. (Some are
built as extensions of others - ZF extends FOL, for example - but none
are conservative extensions like HOLCF.)
Really, HOLCF should be listed next to HOL-Nominal, etc. here:
http://isabelle.in.tum.de/dist/library/HOL/index.html
Email Gateway (Aug 18 2022 at 16:29):From: Tobias Nipkow <nipkow@in.tum.de>
It would also solve my problem that I tend to forget to test HOLCF after
changing HOL.
Tobias
Jasmin Blanchette schrieb:
Email Gateway (Aug 18 2022 at 16:30):From: Makarius <makarius@sketis.net>
These categories are exactly correlated with the directory structure.
Toplevel entries show up in the 2 upper index files, sub-sessions of these
in the lower one.
Changes of the toplevel structure always require various manual adaptions
in administrative scripts, that might also take some time to stabilize.
Whatever is done should we well thought out, and happen not too shortly
before a release deadline.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC