Re: [isabelle] Isabelle Foundation & Certification




On 16/09/2015 17:48, Andrei Popescu wrote:
Dear All,

As far as I know, the integration of Ondra's solution patch is in Makarius's TODO list. Before doing the integration, Makarius wanted to see a mathematical justification for why our solution is sound.
Now such a justification is provided in our ITP paper^[*], in conjunction with Ondra's CPP paper^[**]  -- it is not formal, but quite rigorous. So I see no major impediment to adopting our solution.>

Let us hope you are right, although Makarius was dismissive of what you proved in earlier discussions and wanted a conservativity result.

Moreover, the check that Ondrej implemented is clearly necessary to ban these cicularities.

Of course, it would be great if this were given a higher priority.

That is the whole point. This is not a minor issue with fonts but concerns and endangers the very core of what we are doing.

Tobias

Just for the record, please also note that inconsistencies are not so infrequent in proof assistants: some of the prominent cases of such "incidents" are collected in our ITP paper, under the heading "Inconsistency Club."

[*] http://www.eis.mdx.ac.uk/staffpages/andreipopescu/pdf/ITP2015.pdf

[**] http://www4.in.tum.de/~kuncar/documents/kuncar-cpp2015.pdf

All the best,
    Andrei



---------------------------------------------------------------------------


Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.

If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS.  There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.