Hello all, I’d like to report some progress about CCS in latest HOL.
Soon after my initial post, professor Monica Nesi contacted me privately and she finally found and sent me all those HOL scripts. I still wanted to port her old scripts written in 1992 (25 years ago) in HOL88 (or HOL90, I’m not sure, that ML is even not Standard ML) to HOL4. My motivation is to better understand CCS and finally pass my exam (so far I haven’t). At that time I haven’t learnt to use HOL4, nor Standard ML, so I need to learn these tools and the underlying logics (and lambda calculus, type theory) first. Now I’m doing several parallel projects using HOL4. Since yesterday I started to port these old HOL code into HOL4, and I found this process is so easy (comparing to migration of Coq scripts): the HOL logic didn’t change, most of proof steps work directly in HOL4 without modification, and if I use PROVE_TAC (or METIS_TAC) the proof steps can be greatly reduced. The way to define new fundamental data types using “define_new_type_bijections” is exactly the same as in 25 years ago, just with some syntax changes. It seems that, the concept of “bisimulation” (part of CCS) depends on co-induction. But 25 years ago there was no such support in HOL at all. I hope during the porting work, the new API “Hol_coreln” could be used to simplify the old CCS implementation. A initial snapshot for my porting (only 160 lines) can be found here [1]. I really hope at the end these code could live inside HOL4’s “src” or “example” directories. I believe these code could finally replace the position of The Edinburgh Concurrency Workbench [2]. And after all the CCS theory was invented by Robin Milner, who the same person also invented ML language and LCF, and the latter becomes HOL. And these proof scripts are NOT my original work, they all belong to Professor Monica Nesi. I just do the porting. Regards, Chun Tian [1] https://github.com/binghe/informatica-public/blob/master/CCS/CCSScript.sml [2] http://homepages.inf.ed.ac.uk/perdita/cwb/ > Il giorno 04 giu 2016, alle ore 00:35, Michael Norrish > <michael.norr...@nicta.com.au> ha scritto: > > I think modern machinery would probably make a mechanisation that old seem > extremely long-winded and painful. Even if you found the material, which > seems unlikely, it might not be that helpful. Papers describing it would > probably be good to read though... > > Michael > > On 24 May 2016, at 23:34, Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > >> Hello, >> >> (I'm a school student trying to do some course projects using HOL-4) >> >> Monica Nesi ever wrote a Cambridge tech report called "A formalization of >> the process algebra CCS in high order logic" [1] in 1992, in which he (or >> she) formalized Robin Milner's CCS in HOL. I wonder if the related HOL >> theory scripts are still available somewhere on Internet? >> >> Regards, >> >> -- >> Chun Tian (binghe) >> University of Bologna, Italy >> >> [1] http://128.232.0.20/techreports/UCAM-CL-TR-278.pdf >> ------------------------------------------------------------------------------ >> Mobile security can be enabling, not merely restricting. Employees who >> bring their own devices (BYOD) to work are irked by the imposition of MDM >> restrictions. Mobile Device Manager Plus allows you to control only the >> apps on BYO-devices by containerizing them, leaving personal data untouched! >> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info > > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments.
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
