Jason (jcreed) wrote,
Jason
jcreed
Frank talked a bit about some work he's been doing with Luis on term assignment for sequent proofs in linear logic, with the terms being pi-calculus processes. I find it rather mysterious but quite interesting, for as I mentioned in an email to drl and wjl, I think I usually think of the pi calculus not as a functional programming language, but as a logic programming language --- I can't really account for the peculiar symmetric negotiation between reads and writes that the synchronous pi calculus does (if I remember right) but execution of process P in the asynchronous pi calculus seems to be utterly explainable-away as focusing proof search for a proof of P* |- 1, given the translation
(P + P)*  = (P* & P*)                                                           
0*        = 1                                                                   
(P | P)*  = P* tensor P*                                                        
(nu x.P)* = exists x . P*                                                       
(!P)*     = !(P*)                                                               
(c(x).P)* = all x . msg(c,x) -o P*                                              
(c<d>)* = msg(c,d)

where the quantifiers range over some first-order domain of "channels", and msg is some positive atom that takes two channels.
Tags: logic, pi calculus
Subscribe

  • (no subject)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Went to a series of maker-y talks hosted by Pivotal. The last one, by the woman who runs Genspace, "New York City's Community Biolab" was pretty…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    switch
    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 0 comments