A Semi-Syntactic Soundness Proof for HM(X)
A Semi-Syntactic Soundness Proof for HM(X)
复制标题
HM(X)的半句法健全性证明
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
F. Pottier
中科院分区：
文献类型：
--
作者：
F. Pottier
该文档为基于通用约束的类型推理框架HM（X）提供了合理的证明。我们的证明是半句法。它由两个步骤组成。第一步是定义地面类型系统，其中多态性是扩展的，并以句法方式证明其正确性。第二步是将HM（X）判断解释为基础系统中的（集合）判断，该判断具有对多态性和约束的逻辑观点。总体而言，该方法可能比纯粹的句法方法更模块化：由于多态性和约束是单独处理的，因此它们不会混乱。但是，它产生的结果略有弱：它仅建立HM（x）的类型声音而不是受试者。
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).