Hi Michael, Thank you very much! Then I’ll create a PR once the work at my side is done.
Best regards, Chun > Il giorno 22 gen 2017, alle ore 23:16, <michael.norr...@data61.csiro.au> > <michael.norr...@data61.csiro.au> ha scritto: > > Hi Chun Tian, > > I agree that a CCS example would be very appealing. > > I’m also very happy that porting the old code is turning out to be pretty > straightforward. > > Best wishes, > Michael > > On 22/1/17, 21:47, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote: > > 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. > > > > ------------------------------------------------------------------------------ > 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
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
