Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] A question about an article about Isabelle/HOL/ZF


view this post on Zulip Email Gateway (Aug 18 2020 at 14:51):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

I have an enquiry about one of the articles about Isabelle/HOL/ZF written
by Alexander Krauss and Andreas Schropp : "A Mechanized Translation from
Higher-Order Logic to Set Theory" [1]. Unfortunately, I am struggling to
find the code and the results associated with the article. In the article,
the authors state that the mechanized translation has been applied to the
main HOL image and HOL’s number theory. Have these results ever appeared
either in the main distribution of Isabelle or in the AFP? Has the ML code
associated with the article ever appeared in the public domain? If so, can
it still be found anywhere?

[1] Krauss A, Schropp A. A Mechanized Translation from Higher-Order Logic
to Set Theory. In: Kaufmann M, Paulson LC, editors. Interactive Theorem
Proving [Internet]. Berlin: Springer; 2010. p. 323–38. (Hutchison D, Kanade
T, Kittler J, Kleinberg JM, Mattern F, Mitchell JC, et al., editors.
Lecture Notes in Computer Science; vol. 6172).

P.S. Unfortunately, I am not certain if I have up-to-date contact details
of the authors. Given that the subject of the paper seems to be a
reasonably fundamental work about Isabelle/HOL, I hope it is not
inappropriate to post my enquiry on the mailing list.

Kind Regards,
Mikhail Chekhov

view this post on Zulip Email Gateway (Aug 21 2020 at 19:29):

From: Alexander Krauss <krauss@in.tum.de>
Hi Mikhail,

You do have the correct contact details, I was just too slow to respond, since I‘m currently traveling :-)

At the time, the sources for that experimental work were not published properly IIRC... I can try find them in my private archive when I‘m back in ~ two weeks, and I‘m happy to share them with you... but in any case it will be very hard to get them to work, since they are basen on a modified Isabelle version that was not an official release (although the changes related to the recording of type class inferences did make it into some later release...)

Alex

view this post on Zulip Email Gateway (Aug 21 2020 at 20:56):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Alexander Krauss/All,

Thank you for your reply.

You do have the correct contact details, I was just too slow to respond,
since I‘m currently traveling :-)

Please accept my apologies for the double posting. Although I received
emails from you from your address at "in.tum.de" in the past, there was
some genuine uncertainty in my mind about whether this address was still in
use. In any case, I do not always receive replies and do not anticipate
that all my emails will be answered. Also, I thought that there is a good
chance that the code is still publicly available from an 'old repository
that everyone at TUM knows about' :-).

At the time, the sources for that experimental work were not published
properly IIRC... I can try find them in my private archive when I‘m back in
~ two weeks, and I‘m happy to share them with you... but in any case it
will be very hard to get them to work, since they are basen on a modified
Isabelle version that was not an official release (although the changes
related to the recording of type class inferences did make it into some
later release...)

Given that the source code is not available publicly, of course, it is
entirely up to you whether and/or when you wish to share it. However, I
have to admit that it is likely that I will find it very helpful even
without being able to run the entire study. As you may be aware, I am doing
further work on Types-to-Sets and other related topics ([1], [2], [3], [4],
https://gitlab.com/user9716869) and some of the implemented features are
closely related to the functionality described in [5] (e.g. elimination of
overloading). I would like to ensure that there is no loss of functionality
in comparison to what has been previously implemented in [5]. Also, without
seeing the implementation, I feel that it is more likely that I might make
some false claims in the literature review about what exactly has been
achieved from the perspective of automation in [5]: while the background
theory and the algorithms are described in detail, there is very little
explanation given about the implementation/UI of the framework that you
describe. Furthermore, I have a concern that it is not uncommon to describe
only brief outlines of algorithms in publications, whereas the
implementation may provide additional functionality/exception handling/etc.
I was also slightly worried that if the code was available publicly, then
someone else might have done further (perhaps, unpublished) work on it.

[1] Kunčar O, Popescu A. From Types to Sets by Local Type Definitions in
Higher-Order Logic. In: Blanchette JC, Stephan Merz, editors. Interactive
Theorem Proving. Cham: Springer International Publishing; 2016. p. 200–18.
[2] Immler F, Zhan B. Smooth Manifolds and Types to Sets for Linear Algebra
in Isabelle/HOL. In: 8th ACM SIGPLAN International Conference on Certified
Programs and Proofs. New York: ACM; 2019. p. 65–77. (CPP 2019).
[3] Immler F. Automation for unverloading definitions [Internet].
isabelle/changeset. 2019. Available from:
http://isabelle.in.tum.de/repos/isabelle/rev/ab5a8a2519b0
[4] Gilcher J, Lochbihler A, Traytel D. Conditional Parametricity in
Isabelle/HOL. TABLEAUX/FroCoS/ITP; 2017; TABLEAUX/FroCoS/ITP.
[5] Krauss A, Schropp A. A Mechanized Translation from Higher-Order Logic
to Set Theory. In: Kaufmann M, Paulson LC, editors. Interactive Theorem
Proving [Internet]. Berlin: Springer; 2010. p. 323–38. (Hutchison D, Kanade
T, Kittler J, Kleinberg JM, Mattern F, Mitchell JC, et al., editors.
Lecture Notes in Computer Science; vol. 6172).

Kind Regards,
Mikhail Chekhov

On Fri, Aug 21, 2020 at 10:28 PM Alexander Krauss <krauss@in.tum.de> wrote:

Hi Mikhail,

Am 18.08.2020 um 16:52 schrieb Mikhail Chekhov <
mikhail.chekhov.w@gmail.com>:

Dear All,

I have an enquiry about one of the articles about Isabelle/HOL/ZF written
by Alexander Krauss and Andreas Schropp : "A Mechanized Translation from
Higher-Order Logic to Set Theory" [1]. Unfortunately, I am struggling to
find the code and the results associated with the article. In the
article,
the authors state that the mechanized translation has been applied to the
main HOL image and HOL’s number theory. Have these results ever appeared
either in the main distribution of Isabelle or in the AFP? Has the ML
code
associated with the article ever appeared in the public domain? If so,
can
it still be found anywhere?

[1] Krauss A, Schropp A. A Mechanized Translation from Higher-Order Logic
to Set Theory. In: Kaufmann M, Paulson LC, editors. Interactive Theorem
Proving [Internet]. Berlin: Springer; 2010. p. 323–38. (Hutchison D,
Kanade
T, Kittler J, Kleinberg JM, Mattern F, Mitchell JC, et al., editors.
Lecture Notes in Computer Science; vol. 6172).

P.S. Unfortunately, I am not certain if I have up-to-date contact details
of the authors. Given that the subject of the paper seems to be a
reasonably fundamental work about Isabelle/HOL, I hope it is not
inappropriate to post my enquiry on the mailing list.

You do have the correct contact details, I was just too slow to respond,
since I‘m currently traveling :-)

At the time, the sources for that experimental work were not published
properly IIRC... I can try find them in my private archive when I‘m back in
~ two weeks, and I‘m happy to share them with you... but in any case it
will be very hard to get them to work, since they are basen on a modified
Isabelle version that was not an official release (although the changes
related to the recording of type class inferences did make it into some
later release...)

Alex


Last updated: Sep 28 2021 at 18:21 UTC