Lambda the Ultimate

Tobin-Hochstandt & Felleisen, "Interlanguage Migration: From Scripts to Programs", (Dynamic Languages Symposium 2006)

As scripts grow into full-fledged applications, programmers
should want to port portions of their programs from script-
ing languages to languages with sound and rich type sys-
tems. 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 con-
sists of modules in the untyped lambda calculus, we prove
that rewriting one of them in a simply typed lambda calcu-
lus 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 im-
poses them on the dynamically typed modules in the form
of behavioral contracts.

See also: Typed Scheme by Sam Tobin-Hochstadt:

...a version of PLT Scheme's core with an "occurrence type system".
.. Next we will develop a cross-language refactoring tool that assists programmers with the task of translating one module in a program system from the untyped language into the typed one. [The paper above] lays out the theoretical framework for this research.

(from Felleisen's Projects page)

We'd like to announce availability of a preliminary, open source, interpreter implementing a small core of the Fortress programming language. This interpreter runs on the JVM. You can download the source code at: http://fortress.sunsource.net/.

Our intention is to grow this implementation over time, with the help of university partners and other interested third parties. We expect that many parts of this interpreter will be used as components of a complete Fortress compiler, which is our long term goal.

Fortress has been discussed here several times.

(Posted by Sukyoung Ryu to the TYPES forum.)