from left field, Re: [POPLmark] Meta-comment

[Don Syme]

Hi all

I'm new to this list, so I've missed all the discussions so far.  I just
wanted to mention that my 1997 thesis, which David mentions below, is
available at
  http://www.research.microsoft.com/~dsyme/reports/thesis-dd.pdf

The "Declare" theorem prover itself is not available on the web, though
given the existence of Poplmark it may be fun to resurrect the code,
especially the "Interactive Declare" visual proof environment (given my
current affiliation the resurrection would no doubt be called "Visual
Declare 2005" :-)  ).  

Until then, some sample HTML-ized Declare proofs and specifications are
available the following link:
 
http://www.research.microsoft.com/~dsyme/java/latest/specifications.html

Apologies if the HTML doesn't display correctly on your browser - I
generated this 7 years ago and it was a bit of a hack job. 

Abstract
--------

This dissertation is concerned with techniques for formally checking
properties of systems that are described by operational semantics. We
describe innovations and tools for tackling this problem, and a large
case study in the application of these tools. The innovations centre on
the notion of "declarative theorem proving", and in particular
techniques for declarative proof description. We define what we mean by
this, assess its costs and benefit, and describe the impact of this
approach with respect to four fundamental areas of theorem prover
design: specification, proof description, automated reasoning and
interaction. We have implemented our techniques as the Declare system,
which we use to demonstrate how the ideas translate into practice. The
case study is a formally checked proof of the type soundness of a subset
of the Java language, and is an interesting result in its own right. We
argue why declarative techniques substantially improved the quality of
the results achieved, particularly with respect to maintainability and
readability.


Thanks
Don

-----Original Message-----
From: David Naumann [mailto:naumann at cs.stevens.edu] 
Sent: 18 May 2005 18:53
To: Discussion forum for the POPLmark challenge
Cc: David Naumann
Subject: from left field, Re: [POPLmark] Meta-comment

On the topic of declarative vs procedural interfaces to theorem provers,
I 
would like to point out the work of Don Syme.  His dissertation title 
should suffice:  Declarative Theorem Proving for Operational Semantics.

My very limited experience is with PVS.  It's interface is similar to
the 
HOL provers in using procedural scripts.  In principle this is 
unattractive, as Kevin points out, but in practice the interesting 
structure of a proof can sometimes be made quite clear in the statement 
and use of key lemmas.  For many purposes, it is the
procedurally-oriented 
provers that currently offer the most automation.

About using PVS for metatheory:  Its semantics relies on ZFC, the 
semantics is less simple that HOL, and it is highly engineered (not for 
metatheory) ---about as far from PRA or FPCC as you can get.  On the
other 
hand, I concur with Benjamin Pierce that our general aim is to "greatly 
increase confidence in the correctness of mathematical arguments across
a 
range of specific topics in PL theory". I used PVS to check soundness of
a 
secure flow analysis for a fragment of Java [Banerjee&Naumann, JFP
15(2); 
the PVS work will appear in TPHOLS].  Is PVS a wacky choice?  Perhaps. 
Am I as confident as I would be had the proofs been checked in HOL or
CoQ? 
Of course not.  Is my confidence increased?  Of course.

Will I use PVS again for such purposes?  Definitely yes, partly because
I 
like coding in a highly expressive logic. The object language semantics
is 
a straightforward denotational one (the second reason for "left field"
in 
my subject line) and it is encoded in PVS quite directly, using
dependent 
types and predicate subtypes.  Greg Morrisett wrote "I still find
modeling 
an abstract machine with a heap, which I want to consider as a partial
map 
from (alpha-varying) labels to values (which may have free occurrences
of 
those labels), to be very awkward to encode."  My noninterference proof
is 
a logical relations argument for a language with dynamic memory 
allocation, so I had to deal with exactly this problem.  Renaming of 
addresses is an integral part of the logical relation, both to account
for 
memory allocation and to account for observation at a given security 
level.  PVS doesn't have a magic strategy "mod by bijective renaming" 
and anyway renaming doesn't factor out so simply from the
noninterference 
property.  But it wasn't very painful to work with the elementary 
definitions and reasoning just as we did in the journal paper.

The CMU folks might make me mend my ways if they've used Twelf to check 
their elegant monadic analysis of information flow [Crary, Kliger, 
Pfenning, JFP 15(2)].

--dave

On Wed, 11 May 2005, Kevin Watkins wrote:
...
> Another question, maybe directed at Jerome Vouillon: I know how to go
> through a Twelf proof, and, clause by clause, transform it into a
> series of lemmas, each of which is based on a rule induction of the
> sort that one sees in POPL papers.  Each clause becomes one case of
> such an induction.  The mapping is easy to explain, and in fact, many
> proofs you have seen in papers written by CMUers recently have arisen
> as just such translations of Twelf proofs.  Is there a similarly
> clean, simple, line-by-line interpretation of the Vouillon solution?
> For example, just to pick a line at random, does the phrase
>
> "simpl; intro H3; rewrite H; trivial; generalize H3; case (get_bound
> e' X); simpl; trivial; intros; discriminate"
>
> correspond to a proof step that one would usually see in a
> pencil-and-paper rule induction?  Can someone (without finding the
> particular place in the Vouillon solution from which this example was
> drawn) tell me precisely what it means?  Or is it only comprehensible
> in terms of the imperative effect it has on Coq's internal proof
> search state at the moment it's invoked?  Can someone explain what the
> effect of, say, reversing "trivial; intros" to "intros; trivial" would
> be?
>
> It may be that my example is unfair because I haven't given enough
> context for the phrase to be understandable in isolation.  (In Twelf,
> of course, one can't understand a clause without seeing the type
> declarations for the syntax that's mentioned in it, and the type
> declarations and modes of the relations used in it.  Presumably in Coq
> one would at least need to see the definitions of the inductive types,
> and such.)  In that case, I'd be interested to know how much context
> is necessary to make the phrase sensible.
>
> Kevin
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>