Re: ``universal use'' languages

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