headers
Albert R. Meyer | 3 Feb 1988 11:48
Picon

[mcvax!poincare.crin.fr!lescanne-G7jGt/awsk+BxCq6J4L4RPGfPQYTmyIHInEUo8CAd8F11kfPl2El976AuCXOyjhBHvxpS6adyelJvR45m2QwIg==

From: mcvax!poincare.crin.fr!lescanne@...
Date: Tue, 2 Feb 88 16:40:30 PST
To: bellegarde@..., bousdira <at> crin.crin.fr, cherifa <at> crin.crin.fr,
        ckirchne@..., gnaedig <at> crin.crin.fr, hally <at> crin.crin.fr,
        hkirchne@..., lescanne <at> poincare.crin.fr, rety <at> crin.crin.fr,
        remy@..., rusi <at> crin.crin.fr, schott <at> crin.crin.fr,
        hermann@..., uhrig <at> crin.crin.fr, rouyer <at> crin.crin.fr,
        megrelis@..., lazrek <at> crin.crin.fr,
        umartin@...,
        meyer@..., puel <at> margaux.inria.fr, huet <at> margaux.inria.fr,
        cousinea@..., lechenadec <at> margaux.inria.fr,
        hardin@..., laville <at> margaux.inria.fr, plaisted <at> unc.edu,
        leo%sbcs.CSNET@..., nachum <at> humus.huji.ac.il,
        hsiang%sbcs.CSNET@..., kulcs!eddy <at> uunet.UU.NET,
        uklirb!smolka@...,
        kapur%albanycs.albany.cs.uiuc.edu@...,
        nipkow@..., guttag <at> larch.lcs.mit.edu,
        garland@..., geocub!siva <at> uunet.UU.NET,
        sakai%icot.jp.CSNET@..., ai.hassan <at> mcc.com,
        stickel@..., goguen <at> csl.sri.com,
        odonnell%gargoyle.uchicago.CSNET@...,
        gdp@..., jouannau <at> lri.lri.fr, cc <at> sun4.lri.fr,
        mzali@..., uklirb!madlener <at> uunet.UU.NET,
        uklirb!avenhauss@..., uklirb!steinbach <at> uunet.UU.NET,
        THEORYNT@..., chalmers!fp <at> uunet.UU.NET, NARROW <at> a.cs.uiuc.edu
Subject: a mailing on termination of rewriting systems

    ----------------------------------------------------------------------
   |  A mailing list on termination of rewriting systems and applications |
    ----------------------------------------------------------------------
(Continue reading)

Permalink | Reply | 0 comments |
headers
goguen | 9 Feb 1988 21:19
Favicon

mailing lists on narrowing, termination and rewriting


Dear Uday,

I agree with the thrust of your argument that the narrowing list may be of
interest to some people who are not also interested in rewriting, because of
its connections with logic programming.  However, I think that this argument
would be much stronger if the focus of your list were a little less narrow.
In particular, why dont you broaden it to include other combinations of
functional and logic programming?  Then I would not be able to argue that
	NARROW <= REWRITING.
Also, this would (presumably) enlarge the circulation of your list, by making
it making it somewhat braoder and more of a public service.

Cheers,
Joseph
-------
Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 18 Feb 1988 18:47
Picon

bu-cs.bu.edu@...

Return-Path: <rmb@...>
Date: Thu, 18 Feb 88 17:25:46 EST
From: rmb%bu-cs.bu.edu@...
To: colloq@...
Subject: BU colloq announcements

			COMPUTER SCIENCE DEPARTMENT
			  College of Liberal Arts
		      111 Cummington Street, room 138
		        Boston, Massachusetts, 02215
			 telephone (617) 353-8919

Date:		Wednesday, February 24, 1988
Time:		10:00 a.m.  (tea at 9:45)
Place:		Room 135 at 111 Cummington Street
Speaker:	Wayne Snyder,
		Department of Computer and Information Science 
		University of Pennsylvania		
Title:		COMPLETE SETS OF TRANSFORMATIONS	
		FOR GENERAL $E$-UNIFICATION

Abstract:
    E-unification is a generalization of unification which permits the
use of equality in theorem proving and logic programming.  Many
special algorithms have been developed in the last decade for special
theories, such as associativity and commutativity, but to date the
problem of unifying terms in the presence of an arbitrary set of
equations been little studied.
   In this talk we present a procedure which is sound and complete for
any theory E, based on the abstract method of transformations on
(Continue reading)

Permalink | Reply | 0 comments |
headers
Giuseppe.Longo | 25 Feb 1988 14:50
Picon

consistency proof

A LITTLE VICTORY FOR MODEL THEORISTS !!

A year and half ago I suggested the following "competition" to my friends,
the topmost experts in the proof-theory of lambda calculus I know. Namely,
consider the extension  lbp  of type-free lambda calculus given by:
add to lambda beta (eta) a fresh constant  p  such that
	pp = p
	pxopx = px   (o  is composition)
	MoM = M  implies  pM = M .
Is  lbp  consistent ?  I suggested that we tried to see whether we
could get first an answer by model-theoretic arguments or by proof-theory.
The problem was inspired by the 
retraction models of higher order calculi (see Amadio&Longo in the
IFIP 1986 volume, Wirsing ed., where the question is raised).  Indeed,
if consistent, lbp  above gives a very simple model of the Tp:Tp  theory and
proves that (even though the "types-as-proposition" analogy in the model is
lost) the equational theory of typed lambda terms in the Tp:Tp theory is still
consistent. This is done, of course, by any retraction based model a' la 
Scott-MacCracken, but (the term model of ) lbp is particularly simple.  Or,
more precisely, any interpretation given by "factorizing via" lbp is so.
Thus the problem, besides being difficult, had some good motivations. 
(Note that, for reduction from left to right, lbp is provably not
Church-Rosser).
Stefano Berardi, a student of mine also visiting CMU, has just found a model
for lbp.  Indeed, by some non trivial work on Scott's domain (and its 
subcategory of Girard's coherent spaces) he has shown:

THEOR (Berardi) Any coherent space which yields a
model of lambda beta yields also a model for lbp.
(Continue reading)

Permalink | Reply | 0 comments |
headers
John Mitchell | 25 Feb 1988 21:07
Picon

1988 FOCS


As a member of the 1988 IEEE symp. on Foundations of
Computer Science program committee, I would like to 
encourage the submission of high quality papers on
logic, semantics, and type-theoretic topics of current
interest. 

John Mitchell
Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 27 Feb 1988 16:16
Picon

theory news circulation

Looks like you have braodcast your reply to the entire THEORYNT.
To whom was it addressed anyway?

TYPES has not been specially active lately, so a small sample of
communciations may have created a skewed impression.  But TYPES is neither
intended to be, nor has it been, focussed on syntactic as opposed to semantic
topics.

Regards, Albert
Moderator, types@...
------------------------------------------
   Date:         Fri, 26 Feb 88 13:48:31 GMT
   Reply-To:     TheoryNet List <THEORYNT%NDSUVM1.BITNET@...>,
Paul Taylor <pt <at> doc.ic.ac.uk>
   Sender: TheoryNet List <THEORYNT%NDSUVM1.BITNET@...>
   From: Paul Taylor <pt@...>

   I susbcribe to Albert Meyer's "types" mailing list, and, looking back
   through it, notice a reference to you.  Most of what I've seen in
   "types" has been syntactic, whereas my interest is in semantics
   (category theory, topos theory, domain theory, models of polymorphism,
   stable domain theory).  Does your column cover this?  If so, may
   I join it?  What other similar lists are there?

   Paul Taylor (Dr),    pt@...,    +44 1 589 5111 x 4980
   Dept of Computing, Imperial College, London SW7 2BZ, UK.
Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 29 Feb 1988 12:24
Picon

pt@...

Date: Mon, 29 Feb 88 11:14:48 GMT
From: Paul Taylor <mcvax!doc.ic.ac.uk!pt@...>
To: meyer@...
Subject: Re:  theory news circulation

it was intended to be addressed to the moderator, whoever that it.
anyway, it seems to be getting some interesting replies
I promissed to put a copy of my thesis in the post for you. The envelope
has been sittin gon my desk for several weeks waiting for some extra
papers. I intend to dispatch it today. sorry for delay.
Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 2 Mar 1988 11:35
Picon

nachum@...

From: Nachum dershowitz <nachum@...>
Date: Wed, 2 Mar 88 13:07:31 JST
To: GIDEON@..., NARROW <at> a.cs.uiuc.edu.bitnet,
        logic@..., rewriting <at> crin.crin.fr.bitnet
Subject: RTA-89 ANNOUNCEMENT

Please forward the attached preliminary announcement to the members of
your electronic lists.

Thanks you--
Nachum

==============================================================================

PRELIMINARY ANNOUNCEMENT
RTA-89

Third International Conference on
Rewriting Techniques and Applications

April 3-5, 1989
Chapel Hill, North Carolina, U.S.A.

===============================================================================

The third biannual Conference on Rewriting Techniques and Applications will
be held in Chapel Hill on April 3-5, 1989.  Papers are being solicited in
any of the following or related areas:

    Algebraic semantics
(Continue reading)

Permalink | Reply | 0 comments |
headers
meyer | 2 Mar 1988 11:36

hello

Let me know if you get this.
Thanks, A.
Permalink | Reply | 0 comments |

Gmane