On 26/05/2020 11:24, Andrei Popescu wrote: > > This message's subject refers to an old thread on the Isabelle mailing > list, from July 2018. This time, I and my coauthor are the > protagonists of some "mistakes and gaps"... > > In impressive recent work, > > https://arxiv.org/abs/2002.10212 > > Johannes Åman Pohjola and Arve Gengelbach have formalized in HOL4 our > model-theoretic proof of consistency for (an abstract representation > of) Isabelle/HOL's logic (http://andreipopescu.uk/pdf/ITP2015.pdf).
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 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
