[Prev][Next][Index][Thread]
A PhD thesis on type inference with subtyping

To: types@cs.indiana.edu

Subject: A PhD thesis on type inference with subtyping

From: Francois Pottier <Francois.Pottier@inria.fr>

Date: Fri, 10 Jul 1998 16:05:40 +0200

Cc: Francois Pottier <fpottier@pauillac.inria.fr>, Roberto.Di.Cosmo@ens.fr, Judicael.Courant@inria.fr, Scott Smith <scott@cs.jhu.edu>, trifonov@cs.jhu.edu, Alex Aiken <aiken@cs.berkeley.edu>, Jens Palsberg <palsberg@cs.purdue.edu>, Didier Remy <didier.remy@inria.fr>, Michel Mauny <Michel.Mauny@inria.fr>, Guy Cousineau <Guy.Cousineau@ens.fr>, JeanPierre Jouannaud <JeanPierre.Jouannaud@lri.fr>, Claude.Kirchner@loria.fr, Dominique.Bolignano@inria.fr, JeanChristophe Filliatre <filliatr@clipper.ens.fr>

DeliveryDate: Fri, 10 Jul 1998 09:06:43 0500
Hello,
I am pleased to announce that my PhD thesis, entitled
"Type inference with subtyping: from theory to practice"
is now available electronically, at the following URLs:
French version: http://pauillac.inria.fr/~fpottier/publis/thesefpottier.ps.gz
English version: http://pauillac.inria.fr/~fpottier/publis/thesisfpottier.ps.gz
Here is a summary of this work:
>From a purely theoretical point of view, type inference for a
functional language with parametric polymorphism and subtyping poses
no difficulties. Indeed, it suffices to generalize the inference
algorithm used in the ML language, so as to deal with type
inequalities, rather than equalities. However, the number of such
inequalities is linear in the program sizewhence, from a practical
point of view, a serious efficiency and readability problem.
To solve this problem, one must simplify the inferred constraints. So,
after studying the logical properties of subtyping constraints, this
work proposes several simplification algorithms. They combine
seamlessly, yielding a homogeneous, fully formal framework, which
directly leads to an efficient implementation. Although this
theoretical study is performed in a simplified setting, numerous
extensions are possible. Thus, this framework is realistic, and should
allow a practical appearance of subtyping in languages with type
inference.
Thank you very much for your interest,

François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/