[Prev][Next][Index][Thread]
Ann: new research report
Hello,
I would like to announce the availability of the following research report,
which presents an alternative proof technique for the existing
constraint-based type system HM(X).
A semi-syntactic soundness proof for HM(X)
François Pottier
ftp://ftp.inria.fr/INRIA/publication/RR/RR-4150.ps.gz
This document gives a soundness proof for the generic constraint-based
type inference framework HM(X). Our proof is
semi-syntactic. It consists of two steps. The first step is to
define a ground type system, where polymorphism is
extensional, and prove its correctness in a syntactic way. The
second step is to interpret HM(X) judgements as (sets of) judgements
in the underlying system, which gives a logical view of polymorphism and
constraints. Overall, the approach may be seen as more modular than a
purely syntactic approach: because polymorphism and constraints are
dealt with separately, they do not clutter the subject reduction
proof. However, it yields a slightly weaker result: it only establishes
type soundness, rather than subject reduction, for HM(X).
--
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/