In this paper, we present a statically typed calculus of functional objects called IsoLate that can reason about a pattern of mixin composition without relying on an explicit fixpoint operation. To accomplish this, IsoLate extends a standard isorecursive type system with a mechanism for checking the “mutual consistency” of a collection of functions, that is, that all of the assumptions about self are implied by the collection itself. We prove the soundness of IsoLate via a type-preserving translation to a calculus with F-bounded polymorphism. Therefore, IsoLate can be regarded as a stylized subset of the more expressive calculus that admits an interesting class of programs yet is easy to implement. In the future, we plan to investigate how other, more complicated forms of mixin composition may be supported by lightweight type systems.

I am an Assistant Professor at the University of Chicago. I am interested in programming language, compiler, and program analysis technology. My recent work has focused on type systems for dynamic languages. For more information about my work, check out my research page for publications and talks.