Overview
Well-known techniques exist for proving the soundness of subtyping relations with respect to type safety. However, completeness has not been treated with widely applicable techniques, as far as we are aware.
This project develops some techniques for stating and proving that a subtyping relation is complete with respect to type safety and applies the techniques to the study of iso-recursive subtyping. The common subtyping rules for iso-recursive types—the “Amber rules”—are shown to be incomplete with respect to type safety. That is, there exist iso-recursive types τ1 and τ2 such that τ1 can safely be considered a subtype of τ2 , but τ1 ≤ τ2 is not derivable with the Amber rules.
This project also defines new, algorithmic rules for subtyping iso-recursive types and proves that the rules are sound and complete with respect to type safety.
Publications
On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types. Jay Ligatti, Jeremy Blackburn, and Michael Nachtigal. ACM Transactions on Programming Languages and Systems (TOPLAS), Vol 39, No 1, Article 4, Pages 1-36. ACM Press, March 2017. Local version. [BibTeX]
Induction on Failing Derivations. Jay Ligatti. Technical Report PL-Sep13. University of South Florida, March 2016. (This is a major revision to the September 2013 version.) [BibTeX]
On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types. Jay Ligatti, Jeremy Blackburn, and Michael Nachtigal. Technical Report. University of South Florida, March 2016. (This is a major revision to the August 2014 version of the technical report, which itself was a major revision of technical report CSE-071012, "Completely Subtyping Iso-Recursive Types", from July 2012.) [BibTeX]
SML implementation of a subtyping algorithm for a language with nat, real, product, (disjoint) sum, function, variable-identifier, and iso-recursive types. This software is released under the GNU GPL.
Acknowledgement
This material is based upon work supported in part by the National Science Foundation under Grant No. CNS-0742736. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.