Formalization of a Polymorphic Subtyping Algorithm

Authors: Jinxu Zhao, Bruno C. D. S. Oliveira and Tom Schrijvers

Paper Information

Title:Formalization of a Polymorphic Subtyping Algorithm
Authors:Jinxu Zhao, Bruno C. D. S. Oliveira and Tom Schrijvers
Proceedings:ITP Papers
Editors: Jeremy Avigad and Assia Mahboubi
Keywords:Type Inference, Higher-Ranked Polymorphism, Functional Programming

ABSTRACT. Modern functional programming languages such as Haskell support sophisticated forms of type-inference, even in the presence of higher-order polymorphism. Central to such advanced forms of type-inference is an algorithm for polymorphic subtyping. This paper formalizes an algorithmic specification for polymorphic subtyping in the Abella theorem prover. The algorithmic specification is shown to be decidable, and sound and complete with respect to Odersky and Laufer's well-known declarative formulation of polymorphic subtyping. While the meta-theoretical results are not new, as far as we know our work is the first to mechanically formalize them. Moreover, our algorithm differs from those currently in the literature by using a novel approach based on worklist judgements. Worklist judgements simplify the propagation of information required by the unification process during subtyping. Furthermore they enable a simple formulation of the meta-theoretical properties, which can be easily encoded in theorem provers.

Talk:Jul 09 17:00 (Session 51C)