Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072475
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:03:50 AM
Last modification on : Thursday, October 22, 2020 - 12:22:01 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:09:29 PM

Identifiers

  • HAL Id : inria-00072475, version 1

Collections

Citation

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

Share

Metrics

Record views

148

Files downloads

510