HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

A Semi-Syntactic Soundness Proof for HM(X)

Abstract : This document gives a soundness proof for the generic constraint-based type inference framework HM(X). Our proof is semi-syntactic. It consists in 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).
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:03:50 AM
Last modification on : Thursday, February 3, 2022 - 11:18:36 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:09:29 PM


  • HAL Id : inria-00072475, version 1



François Pottier. A Semi-Syntactic Soundness Proof for HM(X). [Research Report] RR-4150, INRIA. 2001. ⟨inria-00072475⟩



Record views


Files downloads