headers
Organization CLaPF '97 | 1 Jul 1997 02:13
Picon

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.
Permalink | Reply | 0 comments |
headers
Jean-Yves GIRARD | 1 Jul 1997 15:27
Picon
Favicon

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.
Permalink | Reply | 0 comments |
headers
Vaughan R. Pratt | 1 Jul 1997 18:02
Picon

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)

Permalink | Reply | 0 comments |
headers
Geoff Sutcliffe | 3 Jul 1997 01:45
Picon
Picon

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)

Permalink | Reply | 0 comments |
headers
Mariangiola Dezani-Ciancaglini | 3 Jul 1997 09:07
Picon
Favicon

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)

Permalink | Reply | 0 comments |
headers
ruy | 3 Jul 1997 14:32
Picon

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)

Permalink | Reply | 0 comments |
headers
careers | 8 Jul 1997 20:46
Favicon

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)

Permalink | Reply | 0 comments |
headers
berline | 9 Jul 1997 15:10
Picon
Favicon

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)

Permalink | Reply | 0 comments |
headers
Philip Wadler | 16 Jul 1997 20:39
Favicon

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
-----------------------------------------------------------------------
Permalink | Reply | 0 comments |
headers
Robert Harper | 16 Jul 1997 23:26
Picon
Favicon

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)

Permalink | Reply | 0 comments |

Gmane