[EMAIL PROTECTED] wrote:
> Harry,
> My intuition tells me that some sort of small functional core that
>
> used
>
>> RDF as a sort of typing system might be they way to go for Web Services
>> as a lightweight alternative to BPELWS. It's unclear to me if you can
>> squeeze N3-Proofs into some Curry-Howard isomorphism, but if there is a
>> formal proof theory and proofs can be simplified, it should in theory be
>> possible. Proving it is an entire another matter :) and first of course
>> N3 rules would need to be given a proof theory to underlie and maybe
>> clarify the work it obviously already does in practice.
>>
>
> A similar neutral ground I think could be found with pi-calculus
> in the sense that it can bridge the "declared knowledge" to
> "execution environment" gap and we are testcasing that
> and it again all turns around N3 based proofs.
>
Sounds great = I mean you can construct (I mean, it's the *basic* proof)
lambda from pi, so it's not a similar neutral ground, I think it's the
*same neutral ground*. I just think people might be able to sort of grok
"functional programming" better than the pi-calculus. Again, point me to
any papers or code, and do send me mail when they become available if
they aren't now. This is very relevant to my interests. Clearly N3-based
proofs are *very very very important* so I'll look at them closely.
Modelling them in Isabelle might be the way to go.
> Stay tuned; "the future is longer than the past" :-)
> At this moment we focus around an implementation like
>
> REST
> /\
> || N3
> \/
> ,------------,
> | Codd |
> | /\ |
> | || Yap |
> | \/ |
> | ,--------, |
> | | Euler5 | |
> | '--------' |
> '------------'
>
> http://eulersharp.sourceforge.net/2006/02swap/
> and a whole bunch of test cases.
>
>
Excellent. Great hearing this work exists!
--
-harry
Harry Halpin, University of Edinburgh
http://www.ibiblio.org/hhalpin 6B522426
