Email Gateway (Sep 07 2020 at 14:50): Email Gateway (Sep 07 2020 at 14:50):From: Makarius <makarius@sketis.net>
I have now taken the time to read the paper: great work, and great to see
interactions of the various people (re)working foundations of HOL with adhoc
overloading.
As I understand it, the particulars of the dependency relation and its
construction from the definitional theory are still to be settled.
Just note that the cited paper [20] (Ondřej Kunčar, CPP 2015) slightly
deviates from the actual implementation
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/defs.ML
It would be great if the next wave of formalization could clarify this --- in
a way that I know if and how I should improve the implementation as well.
Makarius
Email Gateway (Sep 08 2020 at 09:11):From: "Aman Pohjola, Johannes (Data61, Kensington NSW)" <Johannes.Amanpohjola@data61.csiro.au>
Thanks for the kind words, Makarius.
You're right that the paper left a gap to be filled there: we prove
consistency under the assumption that definitions do not overlap or have
cycles, but we do not consider how to actually discharge this
assumption. To plug this gap, we are currently working on verifying an
implementation of Ondřej's cyclicity checker and connecting that to our
consistency proof.
I must confess I was not aware of the deviations between the paper and
the implementation in Isabelle, thanks for the pointer to that!
Cheers / Johannes
Last updated: Jul 15 2022 at 23:21 UTC