ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Hybrid Reasoning Literature / Systems / Model Theory

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: "Hassan Aït-Kaci" <hassanaitkaci@xxxxxxxxx>
Date: Sat, 08 Dec 2012 16:33:44 -0800
Message-id: <50C3DC68.4040605@xxxxxxx>
On 12/8/2012 4:03 PM, Obrst, Leo J. wrote:
> Yes, almost by definition you will not have much published research in the 
>model-theoretic implications of procedural attachment, I think. There is 
>limited research in general for denotational semantics of procedural 
>programming. I think you would have to first formulate your procedural 
>language into a declarative language/logic, perhaps a functional programming 
>language. However, mathematical theories, "little theories", ala Bill Farmer's 
>work (he's at McMaster U, CA, I think) may help. Or you might think about SMT, 
>Satisfiability Modulo Theory, reasoners, which are SAT reasoners that bring in 
>theories such as reals, bit vectors, etc. They are kind of constraint logic 
>programming systems.
>
> I also vaguely remember Hoare logic from my formal methods days, that tried 
>to formalize some procedural programming constructs.
>
> Thanks,
> Leo    (01)

You are right: for imperative and stateful languages, a denotational 
semantics will be hard to find (and then will probably rely on the 
lambda or mu calculus - in the line of ML or Haskell).    (02)

However, for a complete and definitive account of most (if not all) 
known praqctical programming language semantics see Bob Harper PFPL book 
(Practical Foundations of Programming Languages - available online 
http://www.cs.cmu.edu/~rwh/plbook/book.pdf).    (03)

This being said one can also find denotational semantics for:    (04)

- Scheme (a "clean" variant of LISP with continuations):
   http://www.appsolutions.com/SchemeDS/ds.html    (05)

- Java (all, except concurrency):    (06)

http://reference.kfupm.edu.sa/content/d/y/dynamic_denotational_semantics_of_java__728846.pdf    (07)

and even:    (08)

- C (a sketch, but apparently the author has worked out full ANSI C):
   http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-2001-dsac.pdf    (09)

-hak    (010)

-- 
http://www.hassan-ait-kaci.net/contactme.html    (011)

Attachment: hak.vcf
Description: Vcard


_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

<Prev in Thread] Current Thread [Next in Thread>