headers
Lori Lynn Avirett-Mackenzie | 1 Oct 1992 21:48
Picon

FPCA '93 Call for Papers


************************ CALL FOR PAPERS *********************************

Conference on Functional Programming Languages and Computer Architecture
			   June 9 - 11, 1993
		    University of Copenhagen, Denmark

Sponsored by ACM SIGPLAN/SIGARCH, in cooperation with the MIT Laboratory
for Computer Science, DIKU (Department of Computer Science, University of 
             Copenhagen), and IFIP Working Group 2.8. 

The sixth conference on Functional Programming Languages and Computer
Architectures will cover the design and theory of functional
programming languages, their applications, and their implementations
on parallel and sequential architectures. Topics include (but are not
limited to): language design, type theory, formal semantics;
compilation techniques for sequential and parallel machines,
compile-time analysis, optimizations, program transformations; partial
evaluation; programming methods; generalizations of the functional
programming paradigm for state, control, non-determinism, and
parallelism; special-purpose functional languages; architectural and
system support for storage management, for garbage collection, and for
input/output in functional languages.  Papers accepted for the
conference must contain material not presented previously in any
formal forum.

Authors are also encouraged to submit papers describing practical
experience gained from writing substantial applications in functional
languages or experience in implementing functional languages.  Such
papers should provide some insight into the ease or difficulty of the
(Continue reading)

Permalink | Reply | 0 comments |
headers
John "C." Mitchell | 2 Oct 1992 21:56
Picon

Anon FTP file for conference scheduling


The purpose of this message is to announce a file for posting
tentative and confirmed conference announcements. The current
orientation is towards conferences and workshops in areas related 
to logic in computer science or overlapping with logic-related 
conferences in some way. However, if other people start using it,
the scope may expand.

The file of conference names and dates is 

   pub/conferences

on the machine

  theory.stanford.edu

This may be read by anyone by anonymous ftp. The protocol for
posting an announcement is described below, in a message that
is stored in conferences-README in the same directory.

This scheme will work only if (1) conference organizers use it,
and (2) postings are of the correct format so that the time involved
in maintaining the list is kept to a minimum. 

John Mitchell

--------------------- conferences-README ----------------------

The file ``conferences'' in this directory contains tentative and
confirmed dates of conferences and workshops, primarily in areas
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jean-Yves Girard | 6 Oct 1992 12:29
Picon
Favicon

CRIM Intensive Course


The following is an announcement of an intensive course
on lambda calculus, type theory, and linear logic 
(taught mostly in French) to be held February 1-5 1993.
If you are interested, please contact Pr. G. Blanc, 
Mathematiques, Faculte des Sciences de Luminy, 163
Avenue de Luminy, 13288 MARSEILLE Cedex O9, 
email : gblanc@...

\documentstyle[11pt]{article}
\begin{document}
\begin{center}
		COURS de DEA INTENSIF au CIRM
	
		lambda-calcul typ\'e et logique lin\'eaire

			1-5 f\'evrier 1993
\end{center}

Le cours fait partie du DEA de math\'ematiques de Marseille ainsi que
du DEA de maths-info; il fait partie de l'unit\'e ``logique et
programmation{''} dont l'autre cours ``programmation par
contraintes{''} est assur\'e par Georges Blanc.  Ce cours intensif,
centr\'e sur une semaine, est ouvert aux \'etudiants d'autres DEA
interess\'es par le lambda-calcul type. La DRED finance des s\'ejours
et des voyages pour une quinzaine d'\'etudiants, qui seront
s\'electionn\'es sur dossier; il est bien entendu possible de
participer au DEA en payant la pension CIRM.  Les \'etudiants
\'etrangers, en particulier europ\'eens, sont les bienvenus, \`a
condition qu'ils puissent suivre des cours pour l'essentiel en fran\c
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carolyn Talcott | 14 Oct 1992 16:33
Picon

revised deadline LASC special issue on continuations


                          Call for papers
         Lisp and Symbolic Computation Special Issue on Continuations

Papers are solicited for a special issue of the Lisp and Symbolic Computation
(LASC) on Continuations.  The notion of continuation is ubiquitous in many
different areas of computer science, including logic, constructive
mathematics, programming languages, and programming.  This special issue is a
followup to CW92 the Workshop on Continuations held in June in San Francisco
[between PLDI and LFP].  Suggested topics are: gaining a better understanding
of the nature of continuations; applications of continuations, and the
relation of continuations to other areas of logic and computer science.

Submissions are due Nov 1 1992.  Authors should submit a full paper plus
a 1-2 page extended abstract summarizing the main contributions.  Submissions 
will be prescreened by members of the CW92 program committee.  Papers passing 
the prescreening will undergo the normal review process.  

[Note the revised deadline is serious -- papers will be sent out
 for secreening on Nov 2/3.]

Submissions should be sent to: 

Jan Zubkoff
Lucid Inc.
707 Laurel Street
Menlo Park, CA 94025
415/329-8400
jlz@...
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carolyn Talcott | 14 Oct 1992 16:33
Picon

revised deadline LASC special issue on continuations


                          Call for papers
         Lisp and Symbolic Computation Special Issue on Continuations

Papers are solicited for a special issue of the Lisp and Symbolic Computation
(LASC) on Continuations.  The notion of continuation is ubiquitous in many
different areas of computer science, including logic, constructive
mathematics, programming languages, and programming.  This special issue is a
followup to CW92 the Workshop on Continuations held in June in San Francisco
[between PLDI and LFP].  Suggested topics are: gaining a better understanding
of the nature of continuations; applications of continuations, and the
relation of continuations to other areas of logic and computer science.

Submissions are due Nov 1 1992.  Authors should submit a full paper plus
a 1-2 page extended abstract summarizing the main contributions.  Submissions 
will be prescreened by members of the CW92 program committee.  Papers passing 
the prescreening will undergo the normal review process.  

[Note the revised deadline is serious -- papers will be sent out
 for secreening on Nov 2/3.]

Submissions should be sent to: 

Jan Zubkoff
Lucid Inc.
707 Laurel Street
Menlo Park, CA 94025
415/329-8400
jlz@...
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin Goldberg | 14 Oct 1992 21:06
Picon

CALL FOR PAPERS: SIGPLAN'93 PLDI


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

			CALL FOR PAPERS
		 ACM SIGPLAN '93 Conference on
	 Programming Language Design and Implementation
            Albuquerque, New Mexico, USA, June 23-25, 1993

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

SIGPLAN '93 continues the series of broad-based language and compiler
design conferences.  The conference will provide a forum for
researchers and developers to learn about current practical and
experimental work across the breadth of the field.  The conference
will emphasize experimental results and experience with the languages
and techniques described.

The conference seeks original papers relevant to practical issues
concerning the design, development, implementation, and use of
programming languages (in contrast to the annual SIGACT/SIGPLAN POPL
Conference, which is oriented more toward foundations). The conference
favors no particular programming paradigm or support architecture.
Conference topics include:

    * compiler construction	    * translation by program transformation
    * interpretation		    * benchmarking and assessment
    * preprocessing		    * translator validation
    * design and use of languages   * programming environments
    * special-purpose languages	    * internal representations
    * optimization for scalar and parallel architectures
(Continue reading)

Permalink | Reply | 0 comments |
headers
Bengt Nordstr|m | 19 Oct 1992 11:15
Picon
Picon

Positions at Chalmers, Gothenburg, Sweden

Phil, could you forward this to types? 

Thanks, 
Bengt

___________________________________________________________________________________

                RESEARCH POSITIONS IN PROGRAMMING LOGIC

The Dept of Computer Science in Gothenburg, Sweden is seeking researchers in
programming logic, type theory and related topics.  The work is going to be done
within the ESPRIT Basic Research Actions TYPES (Types for proofs and programs)
which is involved in the following topics:

 .implementation of Alf, an interactive proof system based on a logical framework,

 .experiments with Alf, in particular derivation of programs and proofs,

 .metamathematical studies of type theories,

 .extraction of programs from constructive as well as classical proofs.

We can offer full-time visiting positions starting from January and lasting 6-12
months - exact dates are negotiable. There are two kinds of postions, a post-doc
for a person who took her Ph.D. during the last five years and a position as a
guest researcher for a more experienced person.

The programming logic group is one of three research groups in the department (the
other groups are working on Functional Languages and Concurrency). This group is
involved in the ESPRIT projects TYPES and CLICS and the ESPRIT working group
(Continue reading)

Permalink | Reply | 0 comments |
headers
Bengt Nordstr|m | 19 Oct 1992 11:15
Picon
Picon

Positions at Chalmers, Gothenburg, Sweden

Phil, could you forward this to types? 

Thanks, 
Bengt

___________________________________________________________________________________

                RESEARCH POSITIONS IN PROGRAMMING LOGIC

The Dept of Computer Science in Gothenburg, Sweden is seeking researchers in
programming logic, type theory and related topics.  The work is going to be done
within the ESPRIT Basic Research Actions TYPES (Types for proofs and programs)
which is involved in the following topics:

 .implementation of Alf, an interactive proof system based on a logical framework,

 .experiments with Alf, in particular derivation of programs and proofs,

 .metamathematical studies of type theories,

 .extraction of programs from constructive as well as classical proofs.

We can offer full-time visiting positions starting from January and lasting 6-12
months - exact dates are negotiable. There are two kinds of postions, a post-doc
for a person who took her Ph.D. during the last five years and a position as a
guest researcher for a more experienced person.

The programming logic group is one of three research groups in the department (the
other groups are working on Functional Languages and Concurrency). This group is
involved in the ESPRIT projects TYPES and CLICS and the ESPRIT working group
(Continue reading)

Permalink | Reply | 0 comments |
headers
Giuseppe Longo | 21 Oct 1992 12:35
Picon
Picon

About parametricity

ABOUT PARAMETRICITY
The Genericity Theorem: a note by

 
        Giuseppe Longo     Kathleen Milsted    Sergei Soloviev

 
BACKGROUND
----------

As is well-known, the second order lambda-calculus (system F) allows
"computing with types", i.e., type variables may be lambda-abstracted
in terms (Lambda X . M), and terms may be applied to types (MA).
In his 71 paper, though, Girard remarked that, under certain circumstances,
input types "cannot modify output values".  More precisely, if one
takes a term  J such that, for types  A  and  B,  JB  is equal to
numeral 1 if  B = A  and is equal to 0 if  B /= A, then  F+J does
not normalize. As a consequence,  J  is not definable in F.  The
point here is that the polymorphic term  J  gives "essentially"
different output terms (different erasures), which live in the same
type, according to the (values of the) input types.

What can we say about arbitrary polymorphic terms  M  of type
ForAll X. D ?  How do they "depend" on input types?  The so-called
"proper" form of implicit and explicit polymorphism of lambda-calculus
(distinguished by Strachey from the so called "ad hoc"  polymorphism,
of, for example, overloading) has been largely investigated.

A semantic criterion for parametricity was proposed by
Reynolds as an invariance property under relations between type values.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andre Scedrov | 27 Oct 1992 16:50

linear logic guide


                    A Brief Guide to Linear Logic  

                            Andre Scedrov 

      Abstract.  An overview of linear logic is given, including 
      an extensive bibliography and a simple example of the close 
      relationship between linear logic and computation.

      Available by anonymous ftp from host ftp.cis.upenn.edu and 
      the file pub/papers/scedrov/guide.dvi . The bibliography is 
      also available separately from pub/papers/scedrov/LL-bib.bib .
Permalink | Reply | 0 comments |

Gmane