1 Jul 1997 02:13

### CLaPF Deadline extension

                   Call for Papers - Deadline extension

CLaPF'97
2nd Latin-American Conference on Functional Programming
http://www-lifia.info.unlp.edu.ar/~lambda

October 3-4, 1997
La Plata, Argentina

(organized within 3rd Congreso Argentino de Ciencias de la Computacion)

Because of a confusion in the calls, it was not clear for many people if
the deadline to the conference was July 1st or July 10th. For that reason,
we will accept every paper received before July 10th.
We apologize for any inconvenience caused by this problem.
Thank you all.

Organizing committee.


1 Jul 1997 15:27

### Affine


What is affine in "affine logic" ? Take the viewpoint of denotational
semantics and consider the intuitionistic version of linear logic, in
terms of coherent spaces or Banach spaces. Then the weakening rule
introduces fake dependencies, eg constant functions, and when we
combine it with additive features, we get more generally affine
functions. That's it.
However, this is slightly problematic :
i) we need to modify the interpretation of the tensor, ie define
E  <at>  F by 1 & (E  <at>  F) = (1&E) \otimes (1&F) ; however this connective
will hardly distribute over \oplus
ii) in presence of the classical symmetry, we need to consider
weakening on both sides, and the situation is rather complex.

So, to sum up, "affine" means that, if we define a denotational
semantics, then it has to be done with affine functions ; but
unfortunately, "affine logic" does not quite live at the level of
denotational semantics... what is loosened up is denotational
semantics, which is rather unpleasant.


1 Jul 1997 18:02

### Re: Affine


From: Vladimir Alexiev <vladimir@...>
Date: 	Thu, 26 Jun 1997 10:21:08 -0600
I think the original question is still not answered: why is
affine logic called affine? I would be very disappointed if the
answer is "because you obtain it by loosening up linear logic a
bit, just like you obtain affine geometry by loosening up
linear geometry a bit". I'd imagine that the *character* of the
two "loosening-ups" should be similar.

Affine logic is linear logic with weakening.  Weakening may be
understood as a form of translation.  The algebraic rationale for
rejecting weakening is that the signature contains a constant which is
preserved by homorphisms.  Weakening is refuted in this way by many
closed categories: pointed sets, abelian groups, finite dimensional
vector spaces, etc.  The binary operation of the latter two also
refutes contraction, which however is ok for pointed sets.  Affine
algebra/geometry is the other way round, having a binary operation that
refutes contraction but no constant refuting weakening (affine
geometry's missing origin).

>From the perspective of Chu spaces over K, weakening asserts the
continuity of the unique function

A -> 1

which is equivalent to the requirement that A\perp contain all K
constants.  For K >= 2 this implies that A contains no constants.

Vaughan Pratt

(Continue reading)

3 Jul 1997 01:45

### CADE trustee nominations


CADE Trustee Nominations and Election

Nominations for two CADE Inc. trustee positions will be accepted by
Mark Stickel (stickel@...) and Neil Murray (nvm <at> cs.albany.edu)
through the end of CADE-14 (13-17 July 1997).

(from the bylaws http://www.cs.albany.edu/~nvm/cade.html#bylaws)
Nominations for Trustee positions may be made by any member of CADE,
in writing, to be received by the Trustees up to or during the next
upcoming CADE conference business meeting.  Two members are required
to make a nomination.  To be eligible, nominees must be AAR members,
must give their permission, and must meet the conditions set forth
in Section 2.2 below.  An election as described in Section 2.3 below
will be held within thirty days of the business meeting for the purpose
of selecting two nominees to become Trustees.

Following is a list of current trustees, with ** marking those leaving
their position after the election.

Alan Bundy
Deepak Kapur
** Donald Loveland
Claude Kirchner (CADE-15 Cochair)
Helene Kirchner (CADE-15 Cochair)
** William McCune (CADE-14 Chair)
Neil Murray (Secretary/Treasurer)
John Slaney (Vice President)
** Mark Stickel (President)


(Continue reading)

3 Jul 1997 09:07

### Workshop on Theories of Types and Proofs


Preliminary Program and Second Call for Contributed Papers

(The deadline for Contributed Papers: July 7th)

Workshop on Theories of Types and Proofs

Satellite Workshop of TACS'97

September 8 - 19, 1997
Tokyo Institute of Technology
Tokyo, Japan
<ttp@...>
http://www.is.titech.ac.jp/ttp/

The aim of this two-week workshop is to exchange ideas and research results
in the area of Theories of Types and Proofs. Researchers interested in this
area are welcome to participate and make contributions to the workshop. The
workshop will consist of a series of lectures, contributed talks, and
discussion hours.

The workshop solicits for contributed papers in the field of theories of
types and proofs and related topics. On-going research works and
already published contributions are also
welcome. If you want to give a talk, please fill in the form below and
send us with an extended abstract (2 - 10 pages, in ps file) by e-mail
to <ttp@...> by July 7. The authors who submit a paper will
be notified of the acceptance/rejection by July 25. If you want just
participate the workshop, please fill the first three lines of the form
below and send it by August 15, 1997. For more information, please send

(Continue reading)

3 Jul 1997 14:32

### WoLLIC'97 - Call for Participation

4th Workshop on Logic, Language, Information and Computation (WoLLIC'97)
August 19-22
Fortaleza (Ceara'), Brazil

Re: Selected submissions and Call for Participation

Enclosed is the list of papers selected (ordered alphabetically by first
author's surname) for presentation at the 4th Workshop on Logic, Language,
Information and Computation (WoLLIC'97), to be held between the 19th (Tutorial
Day) and the 22nd of August 1997 in Fortaleza (Ceara'), Brazil.

The list of selected abstracts is also available from the web page
(http://www.di.ufpe.br/~wollic97).  There you can also find the registration
form, and general information about travel to Fortaleza, as well as the
address of places to stay.

Please pre-register as soon as you can.  You do not need to send any money at
this stage.  You can pay the registration fee at the reception's desk.

With congratulations to the authors of accepted papers, we look forward to
welcoming you all in Fortaleza.

Best wishes,

Yours sincerely,

Ruy de Queiroz
(On behalf of the 4th WoLLIC'97 Organising Committee)

-------------------------------------------------------------------------------

(Continue reading)

8 Jul 1997 20:46

### Research positions in formal methods at Kestrel Institute


[apologies for multiple copies]

-------------------------------------------------
Career Opportunities at Kestrel Institute
in Palo Alto, California (http://www.kestrel.edu)
-------------------------------------------------

Kestrel has openings and is hiring and interviewing now.  We have
several openings in R&D for senior researchers as well as recent
graduates.

About Kestrel Technology
------------------------
Kestrel's focus is on advancing the state-of-the-art in software
development.  We are interested in highly automated design methods
that emphasize correctness, performance, scalability, productivity,
ease of use, and security.  These capabilities arise from the
articulation and incorporation of precise software design knowledge
and principles.

Areas of Interest
-------------------
Toward the goal of advancing the state-of-the-art in software
development, Kestrel is interested in formal and mechanized support
for:

* Specification of software systems
* Refinement / transformation of specifications
* Design evolution

(Continue reading)

9 Jul 1997 15:10

### paper announcement

The preprint entitled :

From Computation to Foundations
via Functions and Application :
The Lambda-calculus and its Webbed Models.

Chantal Berline

is now available, either  by clicking on the right place of my
www-page, which is located at :
http://www.logique.jussieu.fr/www.berline/index.html

or by ftp at :
ftp://ftp.logique.jussieu.fr/pub/distrib/berline/970522survey.dvi.gz

Paper copies (69 p.) are also available, just ask me at :
berline@...

In a few  words :

The paper is both : an introduction to lambda-calculus and its
motivations, aimed for mathematicians, and a survey of the diverse
classes of models of untyped lambda-calculus which can be described
from the structured set of their prime elements (the web). This covers
all classical models, many filter models, and all usual inverse limit
models, which appear as examples under this more tractable
presentation.  Several applications of models are given, and we end
with a lot of open questions, including accessible (and even naive)
questions.


(Continue reading)

16 Jul 1997 20:39

### Type soundness for denotational semantics of state

Mads Tofte's thesis contains a (now classic) proof of type
soundness for a language with state, based upon an operational
semantics.  Where would I go to find the same proof for a
denotational semantics, analogous to Milner's original proof
that well-typed programs cannot go wrong?  Thanks, -- P

-----------------------------------------------------------------------
Philip Wadler                             wadler@...
Bell Laboratories             http://cm.bell-labs.com/cm/cs/who/wadler/
Lucent Technologies                             office: +1 908 582 4004
700 Mountain Ave, Room 2T-304                      fax: +1 908 582 5857
Murray Hill, NJ 07974-0636  USA                   home: +1 908 626 9252
-----------------------------------------------------------------------


16 Jul 1997 23:26

### RE: Type soundness for denotational semantics of state

I don't know of a proof based on denotational semantics; why would one
bother?

Let me mention that Wright and Felleisen and (separately) I gave much
simpler proofs of soundness for languages with references (among other
extensions to core ML) based on operational semantics.  Abadi and Cardelli
have adapted these methods to an object-based language.  No maximal fixed
points or any similar constructions are required for these proofs.

Bob

<at> Article{harper:refs-ipl,
author = 	 "Robert Harper",
title = 	 "A Simplified Account of Polymorphic References",
journal =	 "Information Processing Letters",
year =	 1994,
volume =	 "51",
pages =	 "201--206"
}

<at> Article{wright+:type-soundness-ic,
author = 	 "Andrew K. Wright and Matthias Felleisen",
title = 	 "A Syntactic Approach to Type Soundness",
journal =	 ic,
year =	 1994,
volume =	 115,
number =	 1,
pages =	 "38--94",
month =	 "November"
}

(Continue reading)

Gmane