Re: [Hol-info] [isabelle] More on "References about mistakes and gaps in papers"

[Makarius <mak...@sk...>]

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