Ann: new research report


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

  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