Re: semantic web proof, curry/howard isomorphism, N3/turtle syntax and semantics stuff

jos.deroo@agfa.com 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

Received on Friday, 8 September 2006 00:07:24 UTC