3 Sep 17:26 2002

### PLI 2002 early registration deadline approaching

[This is the last announcement we will send about PLI 2002.  Please
note that the early registration deadline is just over a week away.
We look forward to your participation in the events!]

PLI 2002
Principles, Logics, and Implementations of
High-Level Programming Languages

SEPTEMBER 12, 2002

Pittsburgh, PA, USA
October 3-8, 2002
http://pli2002.cs.brown.edu/

PLI is a confederation of conferences and workshops aimed at the
advancement of high-level programming languages.  This year, PLI
consists of three conferences:

ICFP (International Conference on Functional Programming)
PPDP (International Conference on Principles and Practice of
Declarative Programming)
GPCE (Generative Programming and Component Engineering)

and seven workshops:

PLAN-X (Programming Languages for XML)
Scheme
Rule (Rule-Based Programming)


5 Sep 18:40 2002

### ICFP 2002 early registration deadline approaching

			      ICFP 2002
International Conference on Functional Programming
Pittsburgh, PA, USA
October 4-6, 2002
http://icfp2002.cs.brown.edu

SEPTEMBER 12, 2002
(** Next Thursday!! **)

The ICFP conference provides a forum for researchers and developers to
hear about the latest work on the design, implementations, principles,
and uses of functional programming. The conference covers the entire
spectrum of functional programming, from practice to theory, and from
established functional programming languages (Scheme, ML, Haskell) to
novel language designs and to the functional aspects of
object-oriented or concurrent languages.

ICFP 2002 features invited talks by Brad Myers, J Strother Moore, and
Neil Jones.  The results of the ICFP Programming Contest will also be
announced.

ICFP is part of PLI, a confederation of conferences and workshops
aimed at the advancement of high-level programming languages.  This
year, PLI consists of three conferences:

ICFP (International Conference on Functional Programming)
PPDP (International Conference on Principles and Practice of
Declarative Programming)
GPCE (Generative Programming and Component Engineering)


5 Sep 20:42 2002

Please note that, following several requests, the deadline of the
submissions for the VMCAI'03 conference has been extended. The new

-----------------------------------------------------------------------
|                                                                     |
|                     September 17th, 2002 - firm                     |
|                                                                     |
-----------------------------------------------------------------------

With Apology for Multiple Transmissions

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

CALL FOR PAPERS

Fourth International Conference on
VERIFICATION, MODEL CHECKING, and ABSTRACT INTERPRETATION
(VMCAI'03)
NYU, January 9--11, 2003
URL:  http://www.cis.upenn.edu/vmcai/
-----------------------------------------------------------------------

The purpose of VMCAI is to provide a forum for reserachers from the three
communities (Verification, Model Checking, and Abstract Interpretation)
that will facilitate interaction, cross-fertilization, and the advance of
hybrid methods that combine the three.  With the growing need for formal
tools to reason about complex, infinite-state, and embedded systems,
such hybrid methods are bound to be of great importance.



7 Sep 12:02 2002

### PPDP 2002 - early registration deadline approaching

                             PPDP 2002
Fourth International Conference on Principles
and Practice of Declarative Programming
Pittsburgh, PA, USA
October 6-8, 2002
http://ppdp2002.cs.brown.edu

SEPTEMBER 12, 2002
(** Next Thursday!! **)

PPDP aims to stimulate research on the use of declarative methods in
programming and on the design, implementation and application of
programming languages that support such methods.

In addition to the 18 regular paper presentations, PPDP 2002 features
invited talks by Neil Jones, Catuscia Palamidessi and Janos Sztipanovits.

PPDP is part of PLI, a confederation of conferences and workshops
aimed at the advancement of high-level programming languages.  This
year, PLI consists of three conferences:

GPCE (Generative Programming and Component Engineering)
ICFP (International Conference on Functional Programming)
PPDP (International Conference on Principles and Practice of
Declarative Programming)

and seven workshops:

Erlang


9 Sep 20:25 2002

### Paper announcement: Validation and boolean operations for attribute-element constraints

Dear folks,

We are pleased to announce the availability of our new paper

Validation and boolean operations for attribute-element constraints

by Haruo Hosoya and Makoto Murata.  This paper is concerned with core
algorithms that are needed in implementing a statically typed language
for XML processing.  The PS file of the paper can be retrieved from:

http://www.kurims.kyoto-u.ac.jp/~hahosoya/papers/attelm.ps

Cheers,

Haruo Hosoya
Makoto Murata

----------------------------------------------------------------------
Abstract:

Algorithms for validation and boolean operations play a crucial role
in developing XML processing systems involving schemas.  Although
much effort has previously been made for treating {\em elements}, very
few studies have paid attention to {\em attributes}.  This paper
presents a validation and boolean algorithms for Clark's
attribute-element constraints.  Although his mechanism has a prominent
expressiveness and generality among other proposals, treating this is
algorithmically challenging since naive approaches easily blow up even


11 Sep 12:10 2002

### FOSSACS'03 call-for-papers; deadline Friday October 18

Dear Type Theorists,

I warmly encourage you to submit to FOSSACS 2003.  Type theory has
been a popular topic over the years at FOSSACS.  I attach the
call-for-papers.  The deadline is October 18.  Time to get writing!

Andy.

=============================================================================
Foundations of Software Science and Computation Structures
FOSSACS 2003

A member conference of the
European Joint Conferences on Theory and Practice of Software
ETAPS 2003, Warsaw, April 5-13, 2003 =============================================================================

FOSSACS seeks original papers on foundational research with a clear significance for software science.
The conference invites submissions on theories and methods to support the analysis, integration,
synthesis, transformation, and verification of programs and software systems.

Topics covered include, but are not limited to: algebraic models; automata and language theory;
behavioural equivalences; categorical models; computation processes over discrete and continuous
data; computation structures; logics of programs; modal, spatial, and temporal logics; models of
concurrent, reactive, distributed, and mobile systems; process algebras and calculi; semantics of
programming languages; software specification and refinement; transition systems; type systems and
type theory.

Prior meetings were in Lisbon (1998), Amsterdam (1999), Berlin (2000), Genova (2001), and Grenoble (2002).

INVITED SPEAKER


13 Sep 21:17 2002

### Type inference for object calculi S and S_\forall of "A Theory of Objects"

What is known / expected from the state-of-the-art on type inference for
implicitly typed (a la Curry) counterparts of the second-order object
calculi S and S_\forall (16.2 and 16.3 of the book "A Theory of

The calculus in the paper "Type Inference with Simple Selftypes is
NP-complete" by Jens Palsberg seems close to a Curry counterpart of S
with neither variances nor self type parametric elder variable in
redefinition.
What essential differences / challenges are foreseen in tackling S or
S_\forall?

The only other papers on type inference for Abadi and Cardelli's
object calculi I know of are Palsberg's "Efficient Inference of
Object Types" and Henglein's "Breaking the n^3 barrier".
Any other references relevant for inferring types of Curry variants
of S or S_\forall?

Luis Dominguez


16 Sep 12:58 2002

### Type inference and related research...

Hello everyone.

I am a university student in Armenia, preparing for research in the
field of type systems. Being new to research, I am seeking some help
from the scientific community, whose member I will hopefully become
one day. I have two problems. The first problem is figuring out a
direction to do research in (I mean in this particular field), or at
least obtaining a list of open problems and vaguely investigated
areas. And the second problem is how to view "all" the work previously
done in a topic that interests me, with Internet being the only source
of information. I mean is there a way of having a list of works and
some sort of guarantee that it is complete, is CiteSeer authoritative
enough?

I am acquainted with the subject of type systems in general, and
especially interested in polymorphic type inference and related
topics. I would be very grateful if someone tells me about any poorly
investigated problems in these fields. Maybe there's a particular
problem arisen from some recent investigations that needs to be
solved, or any newly evolving field to be examined. Since this is my
first research in this area, the problem should not be a large or very
sophisticated one, just something worth doing.

I have been looking for a particular direction of research for a
while, and have found a few so far. One such direction is so-called
soft typing with its possible variations, another one is alternative
or complementary (to Milner) methods of inferring types. I have found
out that these topics are more or less developed. I do have some more
problems in mind, such as investigating the class of typeable
(type-inferrable) terms, or trying to apply typing or type inference


16 Sep 14:25 2002


Types readers may be interested in these two papers about types and
continuations, which will appear in Higher-Order and Symbolic Computation.

Regards,

Hayo

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

Josh Berdine, Peter O'Hearn, Uday Reddy and Hayo Thielecke:
"Linear Continuation-Passing"

Abstract.  Continuations can be used to explain a wide variety of control
be-haviours, including calling/returning (procedures), raising/handling
(exceptions), labelled jumping (goto statements), process switching
(coroutines), and backtrack-ing.  However, continuations are often
manipulated in a highly stylised way, and we show that all of these, bar
backtracking, in fact use their continuations linearly; this is formalised
by taking a target language for CPS transforms that has both
intuitionistic and linear function types.

http://www.cs.bham.ac.uk/~hxt/research/LinCP.pdf

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

Hayo Thielecke:
"Comparing Control Constructs by Double-barrelled CPS"

Abstract. We investigate call-by-value continuation-passing style


16 Sep 17:08 2002

### Re: Type inference and related research...

Hello,

If your interest is directed towards type systems of real-world programming
languages, focusing on type inference is not necessarily the most productive
direction to take.  As I see it, the subject mostly dead-ends around the
point of sophistication of the Haskell type system, after which it becomes
undecidable or at least unwieldy.  This does not seem like a feature that
will make it into future programming languages that are widely used.
Though, the underlying concept of unification is very powerful and seem more
promising -- if unification is your primary interest, then it could be very
useful to explore it in other, more practical, situations than
type-inference algorithms.

Here are two type-theoretic subjects that I feel hold the most promise
towards improving future type systems:

1. The representation of "very dependent types", as originated by Jason
Hickey.  See http://www.cs.caltech.edu/~jyh/papers/fool3/default.html for
the original paper.  In earlier type systems, terms could reference (by
symbolic binding or de Bruijn index) the 'parameter' part of outer lambda
expressions.  Very dependent types also expose the 'function' part of outer
lambda expressions, but in a more general way than the recursive mu binder:
they preserve partially-known information.

Thus you can use very dependent types to form arbitrarily complex
dependent-typed records with recursive dependencies.  This provides a
framework that seems an ideal framework for representing object-oriented
concepts such as self-type dependence (without resorting to a new binder as
in Cardelli's object calculi), as well as uniformly representing dependent
mathematic structures such as groups or rings.  In my experience, very