BABYL OPTIONS: -*- rmail -*-
Version: 5
Labels:
Note: This is the header of an rmail file.
Note: If you are seeing it in rmail,
Note: it means the file has no messages in it.
1, forwarded,,
Summary-line: 4-Feb clt@SAIL.Stanford.EDU #LFP94 submission
Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130])
by amber.ccs.neu.edu (8.6.4/8.6.4) with SMTP id MAA26035
for <wand@ccs.neu.edu>; Fri, 4 Feb 1994 12:06:36 -0500
Received: by SAIL.Stanford.EDU (5.57/25-eef) id AA28028; Fri, 4 Feb 94 09:06:38 -0800
Date: Fri, 4 Feb 94 09:06:38 -0800
From: Carolyn Talcott <clt@SAIL.Stanford.EDU>
Message-Id: <9402041706.AA28028@SAIL.Stanford.EDU>
To: wand@ccs.neu.edu
Subject: LFP94 submission
*** EOOH ***
Date: Fri, 4 Feb 94 09:06:38 -0800
From: Carolyn Talcott <clt@SAIL.Stanford.EDU>
To: wand@ccs.neu.edu
Subject: LFP94 submission
Enclosed are comments on your LFP submission entitled
A Little Goes a Long Way: A Simple Tool to Support Denotational Compiler-Correctness Proofs
Most comments were supplied by program committee members.
In some cases they were written by other researchers who were consulted
by the committee.
Please remember that LFP submissions are not formally refereed, and that
committee members had approximately 4 weeks in which to read 30 or more
papers. Hence these comments are unlikely to be as complete as journal
referee reports should be.
Also please remember that in the worst case, the only comments you receive
may be from someone who disagreed with the acceptance decision for your
paper. If you disagree with a technical comment, it may be appropriate to
interpret it as a request for clarification instead.
---------------------------------
What precisely is a lambda-theory?
9,14,15 are not exactly standard references for lambda-calculus and
domain theory. Ref 16 seems to be missing.
p. 9/10 what is meant by user defined rules? Are these the semantic and
compiler rules?
What about proving simulations?
alpha-matching should be related to:
beta-0 unification (D.Miller [1991], A logic programming language with
lambda abstraction, function variables, and simple unification, LNCS 475
pp. 253--281 and T.Nipkow[1991] Higher-order critical pairs. LICS 1991)
and v-unification (C.Talcott[1993] A Theory of Binding Structures and
its Applications to Rewriting, TCS 112 pp. 99--143.)
Special purpose TP, like special purpose programming languages might be
the key to making formal methods usable in practice. This approach could be
especially useful for validating tools that manipulate special purpose
languages. It would be interesting to specify and check the correctness of
this prover, since it is simple enough for such a project to be feasible.
In short it seems like a nice, simple idea with lots of potential applications.
---------------------------------
This is a nice self-contained paper that presents a well-defined
problem and a well-defined solution. It could be improved by
a fuller discussion of alpha-matching. Does it have applications
beyond that described in the paper? What is lost from Isabelle's
higher-order unification?
---------------------------------
* Isolating alpha-matching is a good abstraction. You may want to
base the implementation of rewrite systems (extensions of the pure
lambda calculus) on this algorithm. But see below my worries about CR, SN.
* However, O'Donnel's rewriting programming language seems to do
precisely what you want to do. Did you look at it for an alternative?
* If you need more than rewriting (I wouldn't know how to accomodate
the use of the induction hypothesis as a rule), would LCF with its
tactics and tacticals have been the right thing?
* CR and SN of the rewrite system are crucial. If you let
"programmers" supply the rules, who is going to prove that the rules
are CR and SN? Did you prove CR and SN for the rewrite system you
employed?
* You don't mention the work on Mini-ML by Kahn et al in the mid-80s.
If I recall correctly, they used Typol to prove compilers correct.
* Typo in Fig 3: the second ih is applied to e2.
---------------------------------
1, answered,,
Summary-line: 18-Feb clt@SAIL.Stanford.EDU #LFP94 submission >> LASC
Mail-from: From clt@SAIL.Stanford.EDU Fri Feb 18 14:44:57 1994
Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130])
by amber.ccs.neu.edu (8.6.4/8.6.4) with SMTP id OAA17967; Fri, 18 Feb 1994 14:44:55 -0500
Received: by SAIL.Stanford.EDU (5.57/25-eef) id AA10075; Fri, 18 Feb 94 11:44:59 -0800
Date: Fri, 18 Feb 94 11:44:59 -0800
From: Carolyn Talcott <clt@SAIL.Stanford.EDU>
Message-Id: <9402181944.AA10075@SAIL.Stanford.EDU>
To: wand@ccs.neu.edu, gregs@ccs.neu.edu
Cc: kessler@cons.cs.utah.edu
Subject: LFP94 submission >> LASC
Reply-To: clt@SAIL.Stanford.EDU
*** EOOH ***
Date: Fri, 18 Feb 94 11:44:59 -0800
From: Carolyn Talcott <clt@SAIL.Stanford.EDU>
To: wand@ccs.neu.edu, gregs@ccs.neu.edu
Cc: kessler@cons.cs.utah.edu
Subject: LFP94 submission >> LASC
Reply-To: clt@SAIL.Stanford.EDU
I would like to encourage you to submit a journal version of your LFP
submission
A Little Goes a Long Way:
A Simple Tool to Support Denotational Compiler-Correctness Proofs
I liked this paper and think the topic is quite relevant to LASC.
Among other things, it would be a good reinforcement to the
theme of the VLISP issue. The journal version should address the
criticisms of the LFP reviewers. Especially, it should:
discuss work related to alpha-matching, related verification work,
and the issue of build your own vs using existing provers [sad but
probably true, its probably still easier for special cases].
LASC has a new submission procedure which I have appended below,
since its not widely publicized yet. We hope this will improve
the record keeping and speed up the review process.
Best regards,
Carolyn
ps -- Is the prover available for use by others? Could I put a pointer
to it in my database of automated reasoning systems?
==============================================================================
LASC authors should submit two (2) hard copies to:
Mrs. Karen Cullen
LISP AND SYMBOLIC COMPUTATION
Kluwer Academic Publishers
101 Philip Drive
Assinippi Park
Norwell, MA 02061, USA
And electronic copies [ps or dvi format] to one or both of the Co-Editors:
Carolyn Talcott
clt@sail.stanford.edu
and
Robert Kessler
kessler@cons.cs.utah.edu
1,,
Summary-line: 2-Mar to: clt@SAIL.Stanford.EDU #LFP94 submission >> LASC
Received: from delphi.ccs.neu.edu (wand@delphi.ccs.neu.edu [129.10.112.101])
by amber.ccs.neu.edu (8.6.4/8.6.4) with ESMTP id VAA00147; Wed, 2 Mar 1994 21:05:13 -0500
From: Mitchell Wand <wand>
Received: from localhost (wand@localhost)
by delphi.ccs.neu.edu (8.6.4/8.6.4) id VAA07852; Wed, 2 Mar 1994 21:05:12 -0500
Date: Wed, 2 Mar 1994 21:05:12 -0500
Message-Id: <199403030205.VAA07852@delphi.ccs.neu.edu>
To: clt@SAIL.Stanford.EDU
CC: gregs@ccs.neu.edu, kessler@cons.cs.utah.edu
In-reply-to: Carolyn Talcott's message of Fri, 18 Feb 94 11:44:59 -0800 <9402181944.AA10075@SAIL.Stanford.EDU>
Subject: LFP94 submission >> LASC
X-Face: P=+0{wDtTo4h2G):$zxq5=Ta~FSVWTLF=OMK'u$_%T4{oTiRuPdflc#r8}?g
X-Planation: This X-Face is part of the Internet Public Art Project
X-Planation: View it with the 'faces' program
*** EOOH ***
From: Mitchell Wand <wand>
Date: Wed, 2 Mar 1994 21:05:12 -0500
To: clt@SAIL.Stanford.EDU
CC: gregs@ccs.neu.edu, kessler@cons.cs.utah.edu
In-reply-to: Carolyn Talcott's message of Fri, 18 Feb 94 11:44:59 -0800 <9402181944.AA10075@SAIL.Stanford.EDU>
Subject: LFP94 submission >> LASC
Greg and I would be happy to submit a journal version of our LFP paper
A Little Goes a Long Way:
A Simple Tool to Support Denotational Compiler-Correctness Proofs
Greg & his wife are expecting their first child momentarily, so the schedule
for producing a revised version is a little elusive, but we would expect to
get it to you by June. Is that OK?
--Mitch
1,,
Summary-line: 3-Mar clt@SAIL.Stanford.EDU #LFP94 submission >> LASC
Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130])
by amber.ccs.neu.edu (8.6.4/8.6.4) with SMTP id LAA12591; Thu, 3 Mar 1994 11:59:28 -0500
Received: by SAIL.Stanford.EDU (5.57/25-eef) id AA13890; Thu, 3 Mar 94 08:59:32 -0800
Date: Thu, 3 Mar 94 08:59:32 -0800
From: Carolyn Talcott <clt@SAIL.Stanford.EDU>
Message-Id: <9403031659.AA13890@SAIL.Stanford.EDU>
To: wand@ccs.neu.edu
Cc: gregs@ccs.neu.edu, kessler@cons.cs.utah.edu
In-Reply-To: Mitchell Wand's message of Wed, 2 Mar 1994 21:05:12 -0500 <199403030205.VAA07852@delphi.ccs.neu.edu>
Subject: LFP94 submission >> LASC
Reply-To: clt@SAIL.Stanford.EDU
*** EOOH ***
Date: Thu, 3 Mar 94 08:59:32 -0800
From: Carolyn Talcott <clt@SAIL.Stanford.EDU>
To: wand@ccs.neu.edu
Cc: gregs@ccs.neu.edu, kessler@cons.cs.utah.edu
In-Reply-To: Mitchell Wand's message of Wed, 2 Mar 1994 21:05:12 -0500 <199403030205.VAA07852@delphi.ccs.neu.edu>
Subject: LFP94 submission >> LASC
Reply-To: clt@SAIL.Stanford.EDU
Great! I'm glad you decided to do this.
June is fine. There is no special deadline, but of course the sooner
you get it to us, the sooner we can get it in the pipeline.
Carolyn