Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Is there any omega-cpo library in Isabelle

Email Gateway (Aug 11 2023 at 10:56):

From: Xueying Qin <Xueying.Qin@ed.ac.uk>
Hi Isabelle-users,

I am currently working on proving some properties of a formalised semantics in Isabelle.

Since we modelled our semantics using an omega-cpo, we would like to know if there is any exiting Isabelle library of an omega-cpo that we can use?

PS: We have previously tried HOLCF, however since we cannot stay entirely within the HOLCF library it seems not to be a feasible option.

Thanks in advance for any suggestions.

Kind regards,
Xueying Qin
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

Email Gateway (Aug 17 2023 at 19:44):

From: Xueying Qin <Xueying.Qin@ed.ac.uk>
Hi Akihisa,

Thank you very much for your suggestions!

We will certainly have a look at the library and see if it is feasible.

We are currently using the Complete_Partial_Order library for the mechanisation. However such approach does not maintain the continuity assumptions therefore potentially creates some “junk” in our semantics, hence we would like to switch to an omega-cpo.

Kind regards,
Xueying

Last updated: Apr 28 2024 at 20:16 UTC