TABLEAUX'97 Call for Papers

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

[ A separate Call for Tutorials follows the Call for Papers. ]

[ Apologies to those who receive this many times through different channels ]

Dear colleague,

Please find enclosed the Call for Papers
(ascii and latex files) for the conference
TABLEAUX'97 - Analytic Tableaux and Related Methods - that will be
held in Abbaye des Premontres, Pont-a-Mousson (near Nancy), France,
May 13-16, 1997.

Deadline for submissions: November 22, 1996.

Best regards

Didier Galmiche

                        CALL FOR  From types-dist-request@dcs.gla.ac.uk  Sun Jul 28 16:54:21 1996
Return-Path: <types-dist-request@dcs.gla.ac.uk>
Received: from vanuata.dcs.gla.ac.uk by theory.lcs.mit.edu (5.65c/TOC-1.2S) 
	id AA28541; Tue, 30 Jul 96 18:36:18 EDT
Resent-Message-Id: <199607302236.AA28541@theory.lcs.mit.edu>
Message-Id: <199607302236.AA28541@theory.lcs.mit.edu>
Received: from dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk 
          id <03100-0@vanuata.dcs.gla.ac.uk>; Tue, 30 Jul 1996 23:09:57 +0100
From: Alex Aiken <aiken@CS.Berkeley.EDU>
Subject: paper on representations of polymorphic types with subtyping
Date: Sun, 28 Jul 1996 23:54:21 -0700
To: types@dcs.gla.ac.uk
Old-Resent-From: types-request@dcs.gla.ac.uk
Errors-To: types-request@dcs.gla.ac.uk
Approved: types@dcs.gla.ac.uk
Resent-Date:  Tue, 30 Jul 1996 23:09:57 +0100
Resent-From: types@dcs.gla.ac.uk
Resent-To: types-dist@dcs.gla.ac.uk

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

  Jens Palsberg, Ed Wimmers, and I have written a paper "Optimal
Representations of Polymorphic Types with Subtyping", available from

In the Hindley/Milner type system, two polymorphic types are equal if
and only if they are identical up to renamings of quantified
variables.  In a polymorphic type system with subtyping, polymorphic
types can be equal even if they are not structurally similar.  We show
that optimal representations of polymorphic types---where optimal means
a type with a minimum number of quantified variables---can be computed
for some interesting type systems.  The full abstract is below.

Alex Aiken


Many type inference and program analysis systems include notions of
subtyping and parametric polymorphism. When used together, these two
features induce equivalences that allow types to be simplified by
eliminating quantified variables. Eliminating variables both improves
the readability of types and the performance of algorithms whose
complexity depends on the number of type variables. We present an
algorithm for simplifying quantified types in the presence of
subtyping and prove it is sound and complete for non-recursive and
recursive types. We also show that an extension of the algorithm is
sound but not complete for a type language with intersection and union
types, as well as for a language of constrained types.