Coherence of subsumption

Abstract

Subsumption used in subtyping breaks the term-as-proofs paradigm. Semantics most naturally are associated with proofs. Thus a problem of coherence arises: different typing proofs of the same term must have related meanings. We propose a proof-theoretical, rewriting approach to this problem. We focus on F≤, a second order lambda calculus with bounded quantification, which is rich enough to make the problem interesting. We define a normalizing rewrite system on the proofs, in which different proofs of the same typing judgement are transformed in a unique normal proof, and in which normal proofs of judgements assigning different types to the same term are strongly related. This rewriting system is not defined on the proofs themselves but on the terms of an auxiliary type system, in which the terms carry a complete information about their typing proof. This technique gives also a simple proof of the existence of a minimum type for each term. From an analysis of the proofs in normal form we obtain a deterministic type-checking algorithm, which is sound and complete by construction.