From: Dan Connolly (connolly@w3.org)
Date: 02/01/01
"Peter F. Patel-Schneider" wrote: > > Frank mentioned that one possibility for DAML+OIL was to be a language for > ``universal use''. I strongly agree with Ian that that was *not* our charter. > Further, I would be interested in seeing if anyone has either > 1/ a language that is intended for such ``universal use'', or The first time Tim and I found something pretty close to what we want was the PCA paper: [PCA] Proof-Carrying Authentication. Andrew W. Appel and Edward W. Felten, 6th ACM Conference on Computer and Communications Security, November 1999. http://www.w3.org/DesignIssues/Logic#PCA the logic in there is based on a logic framework that looks pretty hairy... one of these typed lambda calculus thingies. There's a proof-checker in 13130 lines of C code, with integrated digital signature support, but the style of C is sorta ML-ish, and I don't really grok. http://foxnet.cs.cmu.edu/pcc/oct98.html But there's lots of related work... proof checkers based on typed lambda calculus are evidently pretty commonplace. Just the other day I found one that runs as an emacs mode: "Boomborg-PC is a proof-checker of Calculus of Constructions that runs on a buffer of GNU Emacs. Calculus of Constructions, proposed by Thierry Coquand and Gerard Huet, is one of the so-called higher-order typed lambda-calculi." -- http://nicosia.is.s.u-tokyo.ac.jp/boomborg/boomborg-pc.html The source code, which includes interactive support in addition to the actual proof checking stuff, is a few KLOC of elisp: 3651 13289 115615 pc.el > 2/ requirements that such a language should meet. > > peter > > PS: By the way, any answer to 1/ would necessarily include an answer to 2/. OK, then I've answered both ;-). But perhaps this more directly answers the question about requirements: The Semantic Web as a language of logic http://www.w3.org/DesignIssues/Logic Or perhaps this scenario illustrates some of the requirements: [[[ 4.Mobile agents. In this set of experiments we extend the safety policy to include resource usage bounds and data abstraction, in addition to memory safety. In a paper to appear in a special LNCS issue on mobile-code security, we describe the use of PCC to ensure the safety of untrusted agents that access a database of airfares. Such agents are assigned an access level when they are received and are required to look only at those database records whose access level is smaller. This requirement is not enforced at run-time, but instead it is a part of the proved safety properties. In addition, the agents must prove that they terminate within a given number of instructions, and if they send network packets, they are not exceeding a preset bandwidth. For an example agent using this safety policy, the proof is about 6 times the size of the code. ]]] -- Proof-Carrying Code http://www.cs.berkeley.edu/~necula/pcc.html#implementation Tue, 22 Jun 1999 01:33:41 GMT -- Dan Connolly, W3C http://www.w3.org/People/Connolly/ office: tel:+1-913-491-0501 pager: mailto:connolly.pager@w3.org (put return phone number in from/subject)
This archive was generated by hypermail 2.1.4 : 04/02/02 EST