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 ; 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 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 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 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 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 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 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 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 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