Interlanguage migration

Abstract

As scripts grow into full-fledged applications, programmers should want to port portions of their programs from scripting languages to languages with sound and rich type systems. This form of interlanguage migration ensures type-safety and provides minimal guarantees for reuse in other applications, too.In this paper, we present a framework for expressing this form of interlanguage migration. Given a program that consists of modules in the untyped lambda calculus, we prove that rewriting one of them in a simply typed lambda calculus produces an equivalent program and adds the expected amount of type safety, i.e., code in typed modules can't go wrong. To ensure these guarantees, the migration process infers constraints from the statically typed module and imposes them on the dynamically typed modules in the form of behavioral contracts.