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
