Re: [isabelle] Isabelle Foundation & Certification



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. Of course, it would be great if this were given a higher priority.  

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.





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